[TYPES/announce] postdoctoral position at Wesleyan University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Hi, The Department of Mathematics and Computer Science at Wesleyan University (Middletown, CT, USA) invites applications for a Postdoctoral Research Associate. The postdoc will work with Professors Norman Danner and Dan Licata on the topic of certified cost analysis of functional programs, and have the freedom to pursue their own research agenda as well. Candidates with backgrounds in any of programming languages, logic, algorithms, and proof assistants are especially encouraged to apply. The position is for 1 year, with possibility of renewal for a second year. It is grant-funded, so teaching is not required, but there is a possibility of teaching 1 class per year for applicants who would like to build their teaching portfolio. Please find information on applying for the job here: https://careers.wesleyan.edu/postings/5800 We will review applications as they are received. Thanks, -Dan
[TYPES/announce] Math Research Communities on Homotopy Type Theory, June 4-10, 2017, Snowbird UT
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, This is a reminder that from June 4-10, 2017, there will be a workshop on Homotopy Type Theory, organized as part of the AMS Mathematics Research Communities program and held in the Snowbird Resort in Utah. The goal of the workshop is to bring together advanced graduate students and postdocs having some background in one (or more) areas such as algebraic topology, category theory, mathematical logic, or computer science, with the goal of learning how these areas come together in homotopy type theory, and working together to prove new results. Basic knowledge of just one of these areas will be sufficient to be a successful participant. The organizers are particularly interested in using this workshop as an opportunity to improve the diversity in the HoTT community in all aspects. For more information about the workshop, including the list of sample topics that participants may be working on and the registration information, please see the website: http://www.ams.org/programs/research-communities/2017MRC-1 All accepted into the program will receive financial support (room and board at the Snowbird Resort and up to $650 towards airfare). The application deadline is *March 1st, 2017.* The majority of the positions are allocated to U.S. citizens and people who are affiliated with U.S. institutions, but a smaller number are also open to international participants. If you have any questions, please feel free to contact any of the organizers. Dan Christensen, Chris Kapulkin, Dan Licata, Emily Riehl, Mike Shulman -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to homotopytypetheory+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
[TYPES/announce] Math Research Communities on Homotopy Type Theory, June 4-10, 2017, Snowbird UT
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, We are pleased to announce that from June 4-10, 2017, there will be a workshop on Homotopy Type Theory, organized as part of the AMS Mathematics Research Communities program and held in the Snowbird Resort in Utah. The goal of the workshop is to bring together advanced graduate students and postdocs having some background in one (or more) areas such as algebraic topology, category theory, mathematical logic, or computer science, with the goal of learning how these areas come together in homotopy type theory, and working together to prove new results. Basic knowledge of just one of these areas will be sufficient to be a successful participant. For more information about the workshop, including the list of sample topics that participants may be working on and the registration information, please see the website: http://www.ams.org/programs/research-communities/2017MRC-1 All accepted into the program will receive financial support (room and board at the Snowbird Resort and up to $650 towards airfare). Although the application deadline is *March 1st, 2017,* early registration will be highly appreciated, as it will help us plan the event and ensure that everyone gets the most out of it. The majority of the positions are allocated to U.S. citizens and people who are affiliated with U.S. institutions, but a smaller number are also open to international participants. If you have any questions, please feel free to contact any of the organizers. Dan Christensen, Chris Kapulkin, Dan Licata, Emily Riehl, Mike Shulman
[TYPES/announce] postdoc position at Wesleyan
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Hi everyone, I am looking for a postdoc with me here at Wesleyan. Possible start dates range from this coming fall to the following one. Please email me or submit an application if you're interested! -Dan The Department of Mathematics and Computer Science at Wesleyan University invites applications for a one-year postdoctoral position, that is potentially renewable for a second year, subject to satisfactory performance and available funds. The postdoc will work with Assistant Professor Dan Licata on the topic of homotopy type theory, specifically directed type theory. The successful applicant will be able to pursue his/her own research agenda as well. Teaching is not required, but there may be an opportunity for the postdoc to teach 1 or 2 courses in their first year for additional compensation if they desire to develop their teaching skills and portfolio. Candidates will be expected to have a Ph.D. in hand by the time of appointment. We will review applications until the position is filled; possible start dates range from September 2016 through winter and fall 2017. Applications must be submitted at https://academicjobsonline.org/ajo/jobs/7590. Applications must include a cover letter, curriculum vitae, and brief research statement. At least one (up to three) letters of recommendation should be submitted on academicjobsonline by the recommender, or the applicant may provide the email addresses of referees from whom we will obtain confidential letters of recommendation. Wesleyan University, located in Middletown, Connecticut, does not discriminate on the basis of race, color, religious creed, age, gender, gender identity or expression, national origin, marital status, ancestry, present or past history of mental disorder, learning disability or physical disability, political belief, veteran status, sexual orientation, genetic information or non-position-related criminal record. We welcome applications from women and historically underrepresented minority groups. Inquiries regarding Title IX, Section 504, or any other non-discrimination policies should be directed to: Antonio Farias, VP for Equity & Inclusion, Title IX and ADA/504 Officer, 860-685-4771, afar...@wesleyan.edu.
[TYPES/announce] Deadline Extension: Logical Frameworks and Meta-Languages: Theory and Practice 2016
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Please note that the submission deadline for LFMTP has been extended to Monday, April 18, AoE. Logical Frameworks and Meta-Languages: Theory and Practice Thursday, 23 June 2016 Affiliated with FSCD Porto, Portugal http://dlicata.web.wesleyan.edu/events/lfmtp2016/ Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2016 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy type theory. * Applications of logical frameworks, e.g., in proof-carrying architectures such as proof-carrying authorization. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml, or Agda and logic programming languages such as lambda Prolog or Alpha-Prolog. == Important Dates == Monday, April 18th: EXTENDED Submission deadline Friday, May 13th: Notification to authors Friday, May 27th: Final version due Thursday, June 23rd: Workshop date == Submission == In addition to regular papers, we also solicit "work in progress" reports, in a broad sense. Those do not need to report fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGPLAN style files. The length is restricted to 10 pages for regular papers and 7 pages for "Work in Progress" papers. Accepted regular papers will be included in the proceedings, which will be published in ACM digital library in its International Proceedings series. Submit now at https://easychair.org/conferences/?conf=lfmtp2016 == Program Committee == - Edwin Brady - Gilles Dowek, co-chair - Marcelo Fiore - Andrew Gacek - Olivier Hermant - Chantal Keller - Dan Licata, co-chair - Bernardo Toninho - Makarius Wenzel
[TYPES/announce] Final CFP: Logical Frameworks and Meta-languages: Theory and Practice (LFMTP) 2016
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Logical Frameworks and Meta-Languages: Theory and Practice Thursday, 23 June 2016 Affiliated with FSCD Porto, Portugal http://dlicata.web.wesleyan.edu/events/lfmtp2016/ Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2016 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy type theory. * Applications of logical frameworks, e.g., in proof-carrying architectures such as proof-carrying authorization. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml, or Agda and logic programming languages such as lambda Prolog or Alpha-Prolog. == Important Dates == Friday, April 8th: Abstract deadline Wednesday, April 13th: Submission deadline Friday, May 13th: Notification to authors Friday, May 27th: Final version due Thursday, June 23rd: Workshop date == Submission == In addition to regular papers, we also solicit "work in progress" reports, in a broad sense. Those do not need to report fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGPLAN style files. The length is restricted to 10 pages for regular papers and 7 pages for "Work in Progress" papers. Accepted regular papers will be included in the proceedings, which will be published in ACM digital library in its International Proceedings series. Submit now at https://easychair.org/conferences/?conf=lfmtp2016 == Program Committee == - Edwin Brady - Gilles Dowek, co-chair - Marcelo Fiore - Andrew Gacek - Olivier Hermant - Chantal Keller - Dan Licata, co-chair - Bernardo Toninho - Makarius Wenzel
[TYPES/announce] OPLSS 2016
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Oregon Programming Languages Summer School June 20-July 2, 2016 Eugene, Oregon There are still spaces available at the 15th Annual Oregon Programming Languages Summer School (OPLSS). Please encourage your PhD students, masters students, advanced undergraduates, colleagues, and selves to attend! This year’s program is titled Types, Logic, Semantics, and Verification and features the following courses: * Programming Languages Background — Robert Harper, Carnegie Mellon University and Dan Licata, Wesleyan University * Category Theory Background — Ed Morehouse, Carnegie Mellon University * Logical Relations — Patricia Johann, Appalachian State University * Network Programming — Nate Foster, Cornell University * Automated Complexity Analysis — Jan Hoffman, Carnegie Mellon University * Separation Logic and Concurrency — Aleks Nanevski, Northeastern University * Principles of Type Refinement — Noam Zeilberger, INRIA * Logical relations/Compiler verification — Amal Ahmed, Northeastern University Full information on the courses and registration and scholarships is available at https://www.cs.uoregon.edu/research/summerschool/. For more information, please email summersch...@cs.uoregon.edu. Robert Harper Dan Licata Zena Ariola
[TYPES/announce] CFP: Logical Frameworks and Meta-languages: Theory and Practice (LFMTP) 2016
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Logical Frameworks and Meta-Languages: Theory and Practice Thursday, 23 June 2016 Affiliated with FSCD Porto, Portugal http://dlicata.web.wesleyan.edu/events/lfmtp2016/ Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2016 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy type theory. * Applications of logical frameworks, e.g., in proof-carrying architectures such as proof-carrying authorization. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml, or Agda and logic programming languages such as lambda Prolog or Alpha-Prolog. == Important Dates == Friday, April 8th: Abstract deadline Wednesday, April 13th: Submission deadline Friday, May 13th: Notification to authors Friday, May 27th: Final version due Thursday, June 23rd: Workshop date == Submission == In addition to regular papers, we also solicit "work in progress" reports, in a broad sense. Those do not need to report fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM sigplanconf style files. The length is restricted to 10 pages for regular papers and 7 pages for "Work in Progress" papers. Accepted regular papers will be included in the proceedings, which will be published in ACM digital library in its International Proceedings series. == Program Committee == - Edwin Brady - Gilles Dowek, co-chair - Marcelo Fiore - Andrew Gacek - Olivier Hermant - Chantal Keller - Dan Licata, co-chair - Bernardo Toninho - Makarius Wenzel
[TYPES/announce] Twelf Tutorial: Second Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear Types readers, The early registration deadline for the Twelf Tutorial (and other POPL events) is this week. We have a very interactive program planned, and we would appreciate it if you would register soon so we know how many teaching assistants we'll need. Thanks! -Dan == Tutorial Announcement and Call for Participation Mechanizing Metatheory with LF and Twelf Monday 19 January 2008 Savannah, GA Co-located with POPL 2009 Registration open! (Early registration ends December 19) http://twelftutorial.plparty.org == The Principles of Programming group at Carnegie Mellon University invites you to a tutorial on the use of LF and Twelf for specifying, implementing, and proving properties of programming languages. The tutorial will be a highly interactive introduction to LF and Twelf aimed at programming languages researchers. No prior experience with LF and Twelf is assumed. We will concentrate on two topics: * Representing programming languages in the LF logical framework * Using Twelf to prove properties of those languages Participants will leave the workshop with experience in reading and writing LF representations of programming languages, and experience reading, writing, and debugging Twelf proofs. You can register for the tutorial when you register for POPL 2009.
