HOL with Definitions: Semantics, Soundness, and a Verified Implementation
From MaRDI portal
Publication:2879260
DOI10.1007/978-3-319-08970-6_20zbMath1416.68167OpenAlexW2144280226MaRDI QIDQ2879260
Rob Arthan, Ramana Kumar, Magnus O. Myreen, Scott Owens
Publication date: 8 September 2014
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://kar.kent.ac.uk/38886/1/itp14.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (13)
A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Automating change of representation for proofs in discrete mathematics (extended version) ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ On definitions of constants and types in HOL ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Proof-Producing Reflection for HOL ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Pattern Matches in HOL: ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ A consistent foundation for Isabelle/HOL ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ Model-theoretic conservative extension for definitional theories ⋮ Proof Auditing Formalised Mathematics
Uses Software
This page was built for publication: HOL with Definitions: Semantics, Soundness, and a Verified Implementation
