An Interpretation of Isabelle/HOL in HOL Light

DOI10.1007/11814771_18zbMATH Open1222.68370OpenAlexW1488510713MaRDI QIDQ3613409FDOQ3613409

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

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

Mathematics Subject Classification ID

Cited In (13)

• A logical framework combining model and proof theory
• Title not available (Why is that?)
• 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

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)