The Twelf Proof Assistant

DOI10.1007/978-3-642-03359-9_7zbMath1252.68263OpenAlexW1813304904MaRDI QIDQ3183521

Carsten Schuermann

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_7

Mathematics Subject Classification ID

Related Items

Presentation and manipulation of Mizar properties in an Isabelle object logic, The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, αCheck: A mechanized metatheory model checker, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Twelf, Semantics of Mizar as an Isabelle object logic

Uses Software

• Nuprl

Cites Work

• Towards a mechanized metatheory of standard ML
• A framework for defining logics
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf