Email Gateway (Aug 18 2022 at 13:37): Email Gateway (Aug 18 2022 at 13:37):From: Amy Felty <afelty@site.Uottawa.ca>
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
Last updated: Nov 21 2024 at 12:39 UTC