Cited in
(87)- The practice of logical frameworks
- Categoricity results and large model constructions for second-order ZF in dependent type theory
- Structuring metatheory on inductive definitions
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Mechanizing coinduction and corecursion in higher-order logic
- A fixedpoint approach to implementing (co)inductive definitions
- scientific article; zbMATH DE number 1479608 (Why is no real title available?)
- scientific article; zbMATH DE number 2080009 (Why is no real title available?)
- Final coalgebras as greatest fixed points in ZF set theory
- scientific article; zbMATH DE number 2090314 (Why is no real title available?)
- First steps towards a formalization of forcing
- Layered map reasoning: an experimental approach put to trial on sets
- scientific article; zbMATH DE number 1088221 (Why is no real title available?)
- scientific article; zbMATH DE number 2090316 (Why is no real title available?)
- scientific article; zbMATH DE number 1863388 (Why is no real title available?)
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- Relating two standard notions of secrecy
- scientific article; zbMATH DE number 2185680 (Why is no real title available?)
- Reconsidering pairs and functions as sets
- scientific article; zbMATH DE number 1863389 (Why is no real title available?)
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- The Isabelle Framework
- Generating custom set theories with non-set structured objects
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Interfaces for refining recursion and procedures
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
- MBase: Representing knowledge and context for the integration of mathematical software systems
- scientific article; zbMATH DE number 7649968 (Why is no real title available?)
- Partial Recursive Functions in Higher-Order Logic
- A first-order syntax for the \(\pi\)-calculus in Isabelle/HOL using permutations
- The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
- An approach to literate and structured formal developments
- Combining Type Theory and Untyped Set Theory
- Set theory for verification. II: Induction and recursion
- Set theory for verification. I: From foundations to functions
- HERMES
- Isabelle
- simpleAPL
- ForMaRE
- VSDITLU
- Monotonox
- Metamath
- Lifting
- IsarMathLib
- mini-ML
- ProofScript
- sprfn
- HOLCF
- Depth First Search
- FinFuns
- Logic2CNF
- Presburger Automata
- PROVERB
- ProofPeer
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
- Type inference for ZFH
- A set theory with support for partial functions
- A mechanized translation from higher-order logic to set theory
- Ordinal Partitions
- ZFC_in_HOL
- Wetzels_Problem
- A general mathematics of names
- An embedding of Ruby in Isabelle
- Mechanised computability theory
- Coinductive Formal Reasoning in Exact Real Arithmetic
- Ordinal arithmetic: Algorithms and mechanization
- Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15--20, 2008. Proceedings
- Semantics of Mizar as an Isabelle object logic
- scientific article; zbMATH DE number 1701361 (Why is no real title available?)
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Partial and nested recursive function definitions in higher-order logic
- scientific article; zbMATH DE number 2080191 (Why is no real title available?)
- scientific article; zbMATH DE number 1507190 (Why is no real title available?)
- Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
- Automatic proof and disproof in Isabelle/HOL
- STMM: A set theory for mechanized mathematics
- An algebraic treatment of procedure refinement to support mechanical verification
- A higher-order interpretation of deductive tableau
- Goals and benchmarks for automated map reasoning
- Set theory or higher order logic to represent auction concepts in Isabelle?
- Smooth_Manifolds
- Using a generalisation critic to find bisimulations for coinductive proofs
- Friends with benefits. Implementing corecursion in foundational proof assistants
- ProofScript: proof scripting for the masses
- Program development schemata as derived rules
- Logic for Programming, Artificial Intelligence, and Reasoning
This page was built for software: Isabelle/ZF
