Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09
Latest Publications

TOTAL DOCUMENTS

10

(FIVE YEARS 0)

H-INDEX

4

(FIVE YEARS 0)

Published By ACM Press

9781605585291

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Formalizing a strong normalization proof for Moggi's computational metalanguage

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577834 ◽

2009 ◽

Author(s):

Christian Doczkal ◽

Jan Schwinghammer

Keyword(s):

Strong Normalization

Download Full-text

How can we prove that a proof search method is not an instance of another?

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577838 ◽

2009 ◽

Author(s):

Guillaume Burel ◽

Gilles Dowek

Keyword(s):

Search Method ◽

Download Full-text

A syntactic account of singleton types via hereditary substitution

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577829 ◽

2009 ◽

Author(s):

Karl Crary

Download Full-text

Higher-order abstract syntax in classical higher-order logic

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577826 ◽

2009 ◽

Author(s):

Douglas J. Howe

Keyword(s):

Higher Order ◽

Order Logic ◽

Abstract Syntax ◽

Higher Order Logic

Download Full-text

A practical module system for LF

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577831 ◽

2009 ◽

Author(s):

Florian Rabe ◽

Carsten Schürmann

Keyword(s):

Download Full-text

Theory support for weak higher order abstract syntax in Isabelle/HOL

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577827 ◽

2009 ◽

Author(s):

Elsa L. Gunter ◽

Christopher J. Osborn ◽

Andrei Popescu

Keyword(s):

Higher Order ◽

Abstract Syntax

Download Full-text

Coercive subtyping in lambda-free logical frameworks

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577830 ◽

2009 ◽

Author(s):

Robin Adams

Keyword(s):

Logical Frameworks

Download Full-text

The calculus of nominal inductive constructions

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577836 ◽

2009 ◽

Author(s):

Edwin Westbrook ◽

Aaron Stump ◽

Evan Austin

Download Full-text

Universal algebra over lambda-terms and nominal terms

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577835 ◽

2009 ◽

Author(s):

Murdoch J. Gabbay ◽

Dominic P. Mulligan

Keyword(s):

Universal Algebra

Download Full-text

Higher-order constraint simplification in dependent type theory

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09 ◽

10.1145/1577824.1577832 ◽

2009 ◽

Author(s):

Jason Reed

Keyword(s):

Type Theory ◽

Higher Order ◽

Dependent Type Theory ◽

Order Constraint ◽

Download Full-text