Mechanizing metatheory in a logical framework

DOI10.1017/S0956796807006430zbMath1125.68029MaRDI QIDQ5308093

Daniel R. Licata, Robert Harper

Publication date: 26 September 2007

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

typed \(\lambda\)-calculus

Mathematics Subject Classification ID

Related Items (14)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Operational semantics of resolution and productivity in Horn clause logic ⋮ A canonical locally named representation of binding ⋮ Formalizing adequacy: a case study for higher-order abstract syntax ⋮ A logical framework with higher-order rational (circular) terms ⋮ Syntactic Metatheory of Higher-Order Subtyping ⋮ A consistent semantics of self-adjusting computation ⋮ Canonical HybridLF: extending Hybrid with dependent types ⋮ An insider's look at LF type reconstruction: everything you (n)ever wanted to know ⋮ Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions ⋮ Plugging-in proof development environments usingLocksinLF ⋮ Syntax for Free: Representing Syntax with Binding Using Parametricity ⋮ Implementing a normalizer using sized heterogeneous types ⋮ Term-generic logic

Uses Software

• HOL Light
• Nuprl
• Twelf
• Automath
• PoplMark

Cites Work

• A linear logical framework
• A Representation of Fω in LF
• A framework for defining logics
• Dependent types ensure partial correctness of theorem provers
• On equivalence and canonical forms in the LF type theory

This page was built for publication: Mechanizing metatheory in a logical framework