[TYPES/announce] LFMTP 2009: Call for Participation

[Amy Felty]

                     Call for Participation
            LFMTP 2009: 4th International Workshop on
   Logical Frameworks and Meta-languages: Theory and Practice
               McGill University, Montreal, Canada
                         August 2, 2009
               http://workshops.inf.ed.ac.uk/lfmtp

Affiliated with CADE-22, Montreal, Canada, August 2-7, 2009
Joint event with the 2009 International Workshop on Proof-Search in
Type Theories (PSTT), August 3, 2009

EARLY REGISTRATION DEADLINES
Registration: June 30
On-campus accommodation: June 25

PROGRAM:
9:00-10:00 Session 1
Douglas Howe
Higher-Order Abstract Syntax in Classical Higher-Order Logic

Elsa Gunter 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
Karl Crary
A Syntactic Account of Singleton Types via Hereditary Substitution

Robin Adams
Coercive Subtyping in Lambda-Free Logical Frameworks

Florian Rabe and Carsten Schuermann
A Practical Module System for LF

Jason Reed
Higher-Order Constraint Simplification In Dependent Type Theory

12:30-14:00 Lunch

14:00-15:30 Session 3
Christian Doczkal and Jan Schwinghammer
Formalizing a Strong Normalization Proof for Moggi's Computational
Metalanguage

Murdoch Gabbay and Dominic Mulligan
Algebraic Theories over Higher-Order Terms and Nominal Terms

Edwin Westbrook and Aaron Stump
The Calculus of Nominal Inductive Constructions

15:30-16:00 Break

16:00-17:00 JOINT LFMTP/PSTT INVITED TALK
Gilles Dowek (Ecole Polytechnique and INRIA)
How Can We Prove That a Proof Method is not an Instance of Another?

17:00-17:30 Discussion

The following talk will open the PSTT workshop the next morning.
JOINT LFMTP/PSTT INVITED TUTORIAL
Wilmer Ricciotti (University of Bologna)
Proof-Search in Matita