


default search action
4th LFMTP 2009: Montreal, Canada
- James Cheney, Amy P. Felty:
Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009. ACM 2009, ISBN 978-1-60558-529-1
Session 1
- Douglas J. Howe:
Higher-order abstract syntax in classical higher-order logic. 1-11 - Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu:
Theory support for weak higher order abstract syntax in Isabelle/HOL. 12-20
Session 2
- Karl Crary:
A syntactic account of singleton types via hereditary substitution. 21-29 - Robin Adams
:
Coercive subtyping in lambda-free logical frameworks. 30-39 - Florian Rabe
, Carsten Schürmann:
A practical module system for LF. 40-48 - Jason Reed:
Higher-order constraint simplification in dependent type theory. 49-56
Session 3
- Christian Doczkal, Jan Schwinghammer:
Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal. 57-63 - Murdoch James Gabbay
, Dominic P. Mulligan
:
Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables. 64-73 - Edwin M. Westbrook, Aaron Stump, Evan Austin:
The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings. 74-83
Joint LFMTP/PSTT invited talk
- Guillaume Burel, Gilles Dowek
:
How can we prove that a proof search method is not an instance of another? 84-87

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.