An Interpretation of Isabelle/HOL in HOL Light
From MaRDI portal
Publication:3613409
DOI10.1007/11814771_18zbMath1222.68370OpenAlexW1488510713MaRDI QIDQ3613409
Publication date: 12 March 2009
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11814771_18
Related Items
A FORMAL PROOF OF THE KEPLER CONJECTURE, A logical framework combining model and proof theory, Proof synthesis and reflection for linear arithmetic, A revision of the proof of the Kepler conjecture, A Foundational View on Integration Problems, Formalising foundations of mathematics
Uses Software
