Pages that link to "Item:Q2879260"
From MaRDI portal
The following pages link to HOL with Definitions: Semantics, Soundness, and a Verified Implementation (Q2879260):
Displaying 13 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- Model-theoretic conservative extension for definitional theories (Q2333319) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- Proof-Producing Reflection for HOL (Q2945631) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- Pattern Matches in HOL: (Q2945657) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- Proof Auditing Formalised Mathematics (Q5195266) (← links)
- A FORMAL PROOF OF THE KEPLER CONJECTURE (Q5280247) (← links)
