An Interpretation of Isabelle/HOL in HOL Light

DOI10.1007/11814771_18zbMATH Open1222.68370OpenAlexW1488510713MaRDI QIDQ3613409FDOQ3613409

Sean Mclaughlin

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

Mathematics Subject Classification ID

Cited In (7)

• A logical framework combining model and proof theory
• Lemma Mining over HOL Light
• Proof synthesis and reflection for linear arithmetic
• Formalising foundations of mathematics
• A revision of the proof of the Kepler conjecture
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• A Foundational View on Integration Problems

Uses Software

• Isabelle
• Isabelle/HOL
• PVS
• OCaml
• HOL Light
• Nuprl
• Twelf

This page was built for publication: An Interpretation of Isabelle/HOL in HOL Light

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