Affiliated with CADE-22, August 2-7, McGill University, Montreal, Canada
Joint event with the 2009 International Workshop on Proof-Search in Type Theories (PSTT), August 3, 2009
The proceedings are now available online here.| Joint LFMTP/PSTT invited speaker (Aug. 2): | Gilles Dowek, "How Can We Prove That a Proof Method is not an Instance of Another?" |
| Joint LFMTP/PSTT tutorial speaker (Aug. 3): | Wilmer Ricciotti, "Proof search in Matita" |
EARLY REGISTRATION DEADLINE: June 30, 2009. Registration, accommodation and local information is here.
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. This workshop will bring together designers, implementers, and practitioners working on these areas.
LFMTP 2009 will provide researchers with a forum to review state-of-the-art techniques and to present progress in:
- the automation and implementation of the meta-theory of programming languages and related calculi, particularly work which involves variable binding and fresh name generation;
- the design of proof assistants, automated theorem provers, and formal digital libraries building upon logical framework technology;
- theoretical and practical issues concerning the encoding of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures;
- case studies of meta-programming, and the mechanization of the (meta) theory of descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory will be particularly welcome.
Call for papers
Papers describing contributions on any theoretical or practical aspect of logical frameworks and metalanguages are welcome, including but not limited to the following topics:
- logical framework design
- meta-theoretic analysis
- applications and comparative studies
- implementation techniques
- efficient proof representation and validation
- proof-generating decision procedures and theorem provers
- proof-carrying code
- substructural frameworks
- semantic foundations
- methods for reasoning about logics
- formal digital libraries
Three categories of papers are solicited:
- Category A: Detailed and technical accounts of new research: up to eight pages including bibliography.
- Category B: Shorter accounts of work in progress and proposed further directions, including discussion papers: up to six pages including bibliography and appendices.
- Category C: System descriptions presenting an implemented tool and its novel features: up to four pages. A demonstration is expected to accompany the presentation.
Additional material, such as examples or proofs, may be submitted in clearly marked appendices, or as part of an online technical report accompanying the submission. This material will be considered or ignored at the discretion of the reviewers.
Preliminary proceedings will be distributed to the participants at the workshop. After the workshop, revised papers will be published electronically in the ACM digital library.
Important dates
| Abstract submission | |
| Submission deadline | |
| Author notification | June 15 |
| Final versions due | July 3 |
| Workshop | August 2 |
Submission instructions
Submissions will be accepted electronically using the EasyChair system. Submissions should be formatted in PDF, using the ACM SIGPLAN style guidelines. Submissions must be clearly categorized and follow the length restrictions mentioned above and must use 9pt font size or larger.
Simultaneous submission with another workshop, conference or journal is not allowed.
Further instructions will be made available around one month before the submission deadline.
Organizers
Frédéric Blanqui (INRIA)James Cheney (University of Edinburgh, Co-Chair)
Adam Chlipala (Harvard University)
Amy Felty (University of Ottawa, Co-Chair)
Martin Hofmann (LMU Munich)
Conor McBride (University of Strathclyde)
Marino Miculan (University of Udine)
Alberto Momigliano (University of Edinburgh)
Gopalan Nadathur (University of Minnesota)
Michael Norrish (NICTA)
Preliminary program
| 9:00-10:00 | Session 1: |
| 9:00 | Douglas Howe. Higher-Order Abstract Syntax in Classical Higher-Order Logic |
| 9:30 | Elsa Gunter, Christopher J. Osborn and Andrei Popescu. Theory Support for Weak Higher Order Abstract Syntax in Isabelle/HOL |
| 10:00-10:30 | Break |
| 10:30-12:30 | Session 2: |
| 10:30 | Karl Crary. A Syntactic Account of Singleton Types via Hereditary Substitution |
| 11:00 | Robin Adams. Coercive Subtyping in Lambda-Free Logical Frameworks |
| 11:30 | Florian Rabe and Carsten Schuermann. A Practical Module System for LF |
| 12:00 | Jason Reed. Higher-Order Constraint Simplification In Dependent Type Theory |
| 12:30-2:00 | Lunch |
| 2:00-3:30 | Session 3: |
| 2:00 | Christian Doczkal and Jan Schwinghammer. Formalizing a Strong Normalization Proof for Moggi's Computational Metalanguage |
| 2:30 | Murdoch Gabbay and Dominic Mulligan. Algebraic theories over higher-order terms and nominal terms |
| 3:00 | Edwin Westbrook and Aaron Stump. The Calculus of Nominal Inductive Constructions |
| 3:30-4:00 | Break |
| 4:00-5:00 | Session 4: Invited talk by Gilles Dowek: "How Can We Prove That a Proof Method is not an Instance of Another?" |
| 5:00-5:30 | Wrap up & discussion |
Announcements
8/10/2009: Proceedings published online
6/16/2009: Accepted papers & preliminary program announced
6/8/2009: CADE Registration open
5/4/2009: Deadlines extended
2/13/2009: Invited speaker announced.
2/13/2009: Invited speaker announced.
2/12/2009: Submission instructions posted.
1/16/2009: LFMTP web page posted.