An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf

DOI10.1007/11916277_11zbMath1165.68473OpenAlexW1523064151MaRDI QIDQ5387890

Mark-Oliver Stehr, Carsten Schuermann

Publication date: 27 May 2008

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11916277_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Lax Theory Morphisms, Towards Logical Frameworks in the Heterogeneous Tool Set Hets, The Twelf Proof Assistant, Twenty years of rewriting logic, FoCaLiZe and Dedukti to the rescue for proof interoperability, A pluralist approach to the formalisation of mathematics, Experiences from exporting major proof assistant libraries

Uses Software

• Nuprl
• Twelf