An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
From MaRDI portal
Publication:5387890
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
Related Items (7)
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
This page was built for publication: An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf