Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009 - researchr publication

researchr

You are not signed in
Sign in
Sign up

James Cheney, Amy P. Felty, editors, 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. [doi]

Conference: lfmtp2009

Abstract is missing.

Higher-order abstract syntax in classical higher-order logicDouglas J. Howe. 1-11 [doi]

Theory support for weak higher order abstract syntax in Isabelle/HOLElsa L. Gunter, Christopher J. Osborn, Andrei Popescu 0001. 12-20 [doi]

A syntactic account of singleton types via hereditary substitutionKarl Crary. 21-29 [doi]

Coercive subtyping in lambda-free logical frameworksRobin Adams. 30-39 [doi]

A practical module system for LFFlorian Rabe, Carsten Schürmann. 40-48 [doi]

Higher-order constraint simplification in dependent type theoryJason Reed 0001. 49-56 [doi]

Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominalChristian Doczkal, Jan Schwinghammer. 57-63 [doi]

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variablesMurdoch James Gabbay, Dominic P. Mulligan. 64-73 [doi]

The calculus of nominal inductive constructions: an intensional approach to encoding name-bindingsEdwin M. Westbrook, Aaron Stump, Evan Austin. 74-83 [doi]

How can we prove that a proof search method is not an instance of another?Guillaume Burel, Gilles Dowek. 84-87 [doi]

runs on WebDSL