Pages that link to "Item:Q5477669"
From MaRDI portal
The following pages link to Theorem Proving in Higher Order Logics (Q5477669):
Displaying 10 items.
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL (Q541222) (← links)
- Flyspeck II: The basic linear programs (Q2379683) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL (Q3183537) (← links)
- Formal SOS-Proofs for the Lambda-Calculus (Q5178966) (← links)
- Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? (Q5495927) (← links)
- Formal power series (Q5891671) (← links)
- Effect polymorphism in higher-order logic (proof pearl) (Q5915785) (← links)
- Effect polymorphism in higher-order logic (proof pearl) (Q5919584) (← links)
