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

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

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