Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation

DOI10.1007/s10817-015-9357-xzbMath1356.68194OpenAlexW2339308944WikidataQ59476114 ScholiaQ59476114MaRDI QIDQ287361

Ramana Kumar, Magnus O. Myreen, Scott Owens, Rob Arthan

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9357-x

zbMATH Keywords

verificationconsistencytheorem provinghigher-order logicsemanticsinteractive theorem provingHOLself-formalisationself-verification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Formalization of the resolution calculus for first-order logic, Proof-Producing Reflection for HOL, Formalising Mathematics in Simple Type Theory, Proof-producing synthesis of CakeML from monadic HOL functions, Unnamed Item, Programming and verifying a declarative first-order prover in Isabelle/HOL, A verified proof checker for higher-order logic, Unnamed Item, Exercising Nuprl’s Open-Endedness, Isabelle's metalogic: formalization and proof checker, \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic, Formalization of the Resolution Calculus for First-Order Logic, A formalization and proof checker for Isabelle's metalogic

Uses Software

• Isabelle
• ML
• HOL
• HOL Light
• LCF
• CakeML
• Milawa
• Jitawa
• Completeness theorem
• OpenTheory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• A theory of type polymorphism in programming
• An introduction to mathematical logic and type theory: To truth through proof.
• Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings
• Proof-producing translation of higher-order logic into pure and stateful ML
• Towards a Formally Verified Proof Assistant
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• The Reflective Milawa Theorem Prover Is Sound
• HOL Constant Definition Done Right
• HOL Light: An Overview
• A Short Presentation of Coq
• A Brief Overview of HOL4
• The Isabelle Framework
• Towards Self-verification of HOL Light
• Steps towards Verified Implementations of HOL Light
• CakeML
• Theorem Proving in Higher Order Logics
• A Mechanized Translation from Higher-Order Logic to Set Theory
• Completeness in the theory of types