An Interpretation of Isabelle/HOL in HOL Light

DOI10.1007/11814771_18MaRDI QIDQ3613409zbMATH OpenOpenAlexFDO

Authors 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

Recommendations

• Importing HOL Light into Coq
• HOL Light: An Overview
• The Isabelle Framework
• Towards Self-verification of HOL Light
• A mechanized translation from higher-order logic to set theory

Cited in

(13)

• A logical framework combining model and proof theory
• scientific article; zbMATH DE number 1424013 (Why is no real title available?)
• Lemma Mining over HOL Light
• Interpreting HOL in the calculus of constructions
• Fast machine words in Isabelle/HOL
• A formal proof of the Kepler conjecture
• A foundational view on integration problems
• Conversion of HOL Light proofs into Metamath
• Proof synthesis and reflection for linear arithmetic
• A mechanized translation from higher-order logic to set theory
• Formalising foundations of mathematics
• A revision of the proof of the Kepler conjecture
• Scalable LCF-style proof translation

Describes a project that uses

Uses Software

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

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)