Program for LFMTP'07

Session 1 : Welcome, Invited Talk, System Description

Session Chair: Carsten Schürmann
9:00 - 10:00   Randy Pollack (University of Edinburgh)
      Invited Talk
10:00 - 10:30   Alberto Momigliano, Alan J. Martin and Amy P. Felty.
         Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax
      System Description

10:30 - 11:00   Break

Session 2: Technology

Session Chair: to be announced
11:00 - 11:30 William Lovas and Frank Pfenning.
         A Bidirectional Refinement Type System for LF
11:30 - 12:00 Paul Callaghan.
         Coercive subtyping via mappings of reduction behaviour
12:00 - 12:30 Brigitte Pientka, Florent Pompigne and Xi Li.
         Focusing the inverse method for LF: a preliminary report

12:30 - 14:00   Lunch

Session 3: Applications

Session Chair: to be announced
14:00 - 14:30 Julien Narboux and Christian Urban.
         Formalisation of the Logical Relation Proof given by Crary for Completeness of Equivalence Checking
14:30 - 15:00 Alexandre Buisse and Peter Dybjer.
         Formalizing Categorical Models of Type Theory in Type Theory
15:00 - 15:30 Michael Zeller, Aaron Stump and Morgan Deters.
         A Signature Compiler for the Edinburgh LF

15:30 - 16:00   Break

Session 4: Meta-Theory

Session Chair: Brigitte Pientka
16:00 - 16:30 Anders Schack-Nielsen.
         Towards a meta-logic for CLF
16:30 - 17:00 Fredrik Lindblad.
         Higher-Order Proof Construction Based on First-Order Narrowing.
17:00 - 17:30 Murdoch Gabbay and Stephane Lengrand..
         The lambda context calculus.


Brigitte Pientka      Carsten Schürmann
School of Computer Science Department of Theoretical Computer Science
McGill University IT University of Copenhagen
bp at cs dot mcgill dot ca carsten at itu dot dk

[ Home | CFP | Program | Organizers | Previous workshops ]
Brigitte Pientka