The following pages link to Isabelle/ZF (Q17120):
Displayed 50 items.
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- Reconsidering pairs and functions as sets (Q286796) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15--20, 2008. Proceedings (Q929188) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings (Q1819255) (← links)
- A set theory with support for partial functions (Q1840647) (← links)
- Structuring metatheory on inductive definitions (Q1854368) (← 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)
- First steps towards a formalization of forcing (Q2333671) (← links)
- Presentation and manipulation of Mizar properties in an Isabelle object logic (Q2364678) (← links)
- A general mathematics of names (Q2373874) (← links)
- An algebraic treatment of procedure refinement to support mechanical verification (Q2576574) (← links)
- (Q2769442) (← links)
- A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations (Q2841231) (← links)
- (Q2917407) (← links)
- Friends with Benefits (Q2988636) (← links)
- (Q3024857) (← links)
- Mechanised Computability Theory (Q3088013) (← 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)
- Coinductive Formal Reasoning in Exact Real Arithmetic (Q3535611) (← links)
- The Isabelle Framework (Q3543647) (← links)
- (Q3586992) (← links)
- Combining Type Theory and Untyped Set Theory (Q3613410) (← links)
- Partial Recursive Functions in Higher-Order Logic (Q3613436) (← links)
- Mechanizing coinduction and corecursion in higher-order logic (Q4340418) (← links)
- (Q4364537) (← links)
- (Q4472192) (← links)
- (Q4472433) (← links)
- (Q4490719) (← links)
- (Q4503910) (← links)
- (Q4520767) (← links)
- An embedding of Ruby in Isabelle (Q4647513) (← links)
- Final coalgebras as greatest fixed points in ZF set theory (Q4719351) (← links)
- (Q4790663) (← links)
- (Q4790664) (← links)
- (Q4809073) (← links)
- (Q4809075) (← links)
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf (Q4827615) (← links)
- Layered map reasoning (Q4923516) (← links)