Pages that link to "Item:Q1319386"
From MaRDI portal
The following pages link to Set theory for verification. I: From foundations to functions (Q1319386):
Displaying 28 items.
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- Reconsidering pairs and functions as sets (Q286796) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- Categoricity results for second-order ZF in dependent type theory (Q1687749) (← links)
- Set theory for verification. II: Induction and recursion (Q1904402) (← links)
- An approach to literate and structured formal developments (Q1911317) (← links)
- Generating custom set theories with non-set structured objects (Q2128829) (← links)
- Categoricity results and large model constructions for second-order ZF in dependent type theory (Q2319994) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Presentation and manipulation of Mizar properties in an Isabelle object logic (Q2364678) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- ProofScript: Proof Scripting for the Masses (Q3179409) (← links)
- Type Inference for ZFH (Q3453108) (← links)
- The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF (Q3507465) (← links)
- The Isabelle Framework (Q3543647) (← links)
- An embedding of Ruby in Isabelle (Q4647513) (← links)
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf (Q4827615) (← links)
- Layered map reasoning (Q4923516) (← links)
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF (Q5001547) (← links)
- A fixedpoint approach to implementing (Co)inductive definitions (Q5210768) (← links)
- Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? (Q5495927) (← links)
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. (Q5875415) (← links)
- (Q5875427) (← links)
- The practice of logical frameworks (Q5878905) (← links)
- Formalization of the fundamental group in untyped set theory using auto2 (Q5915787) (← links)
- MBase: Representing knowledge and context for the integration of mathematical software systems (Q5950933) (← links)
- Combining higher-order logic with set theory formalizations (Q6161232) (← links)
