Proof-producing reflection for HOL. With an application to model polymorphism

DOI10.1007/978-3-319-22102-1_11MaRDI QIDQ2945631zbMATH OpenOpenAlexFDO

Authors Benja Fallenstein, Ramana Kumar

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-22102-1_11

Mathematics Subject Classification ID

Higher-order logic (03B16) Mechanization of proofs and logical operations (03B35) Large cardinals (03E55) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• scientific article; zbMATH DE number 1341617
• scientific article; zbMATH DE number 2185723
• Towards Self-verification of HOL Light
• scientific article; zbMATH DE number 785045
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)

Cites work

• A Brief Overview of HOL4
• An introduction to small scale reflection in Coq
• HOL Light: An Overview
• HOL with definitions: semantics, soundness, and a verified implementation
• scientific article; zbMATH DE number 1342277 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• 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
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• Proof-producing translation of higher-order logic into pure and stateful ML
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• The Four Colour Theorem: Engineering of a Formal Proof
• The Isabelle Framework
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• Towards Self-verification of HOL Light
• Transfinite Progressions: A Second Look at Completeness
• Transfinite recursive progressions of axiomatic theories

Cited in

(5)

• scientific article; zbMATH DE number 1670739 (Why is no real title available?)
• Extensible and efficient automation through reflective tactics
• Comprehending Isabelle/HOL’s Consistency
• scientific article; zbMATH DE number 1341617 (Why is no real title available?)
• scientific article; zbMATH DE number 2090314 (Why is no real title available?)

Describes a project that uses

Uses Software

• HOL Light
• Milawa
• Isabelle
• HOL

This page was built for publication: Proof-producing reflection for HOL. With an application to model polymorphism

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