Pages that link to "Item:Q1319386"

The following pages link to Set theory for verification. I: From foundations to functions (Q1319386):

Displaying 35 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)
• Experimenting with Isabelle in ZF set theory (Q1312157) (← links)
• Set theory for verification. I: From foundations to functions (Q1319386) (← links)
• \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations (Q1319387) (← links)
• Categoricity results for second-order ZF in dependent type theory (Q1687749) (← links)
• The foundation of a generic theorem prover (Q1823013) (← 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)
• A `theory' mechanism for a proof-verifier based on first-order set theory (Q4707766) (← links)
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf (Q4827615) (← links)
• Techniques of computable set theory with applications to proof verification (Q4884662) (← 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)
• A concrete final coalgebra theorem for ZF set theory (Q6061877) (← links)
• On extensibility of proof checkers (Q6061878) (← links)
• Combining higher-order logic with set theory formalizations (Q6161232) (← links)