LFMTP 2009

4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice
McGill University, Montreal, Canada
August 2, 2009

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"
Deadline extension: Abstracts due May 7, papers due May 12

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:

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:

Three categories of papers are solicited:

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 May 1 May 7
Submission deadline May 8 May 12
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.


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:00Douglas Howe. Higher-Order Abstract Syntax in Classical Higher-Order Logic
9:30Elsa 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:30Karl Crary. A Syntactic Account of Singleton Types via Hereditary Substitution
11:00Robin Adams. Coercive Subtyping in Lambda-Free Logical Frameworks
11:30Florian Rabe and Carsten Schuermann. A Practical Module System for LF
12:00Jason Reed. Higher-Order Constraint Simplification In Dependent Type Theory
12:30-2:00 Lunch
2:00-3:30 Session 3:
2:00Christian Doczkal and Jan Schwinghammer. Formalizing a Strong Normalization Proof for Moggi's Computational Metalanguage
2:30Murdoch Gabbay and Dominic Mulligan. Algebraic theories over higher-order terms and nominal terms
3:00Edwin 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


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.