James Cheney, Amy P. Felty (Eds.):
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
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
data released under the ODC-BY 1.0 license
