The Twelf Proof Assistant

DOI10.1007/978-3-642-03359-9_7MaRDI QIDQ3183521zbMATH OpenOpenAlexFDO

Authors Carsten Schürmann

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

Recommendations

• Functional and Logic Programming
• scientific article; zbMATH DE number 2110615
• scientific article; zbMATH DE number 4180831
• scientific article; zbMATH DE number 65531
• Logical frameworks

Cites work

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

Cited in

(13)

• Twelf
• Semantics of Mizar as an Isabelle object logic
• Presentation and manipulation of Mizar properties in an Isabelle object logic
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle
• Categorical properties of logical frameworks
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Logical relations for a logical framework
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• αCheck: A mechanized metatheory model checker
• The -framework
• Functional and Logic Programming
• An open challenge problem repository for systems supporting binders
• Proof search algorithm in pure logical framework

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: The Twelf Proof Assistant

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183521)