The Isabelle Framework
From MaRDI portal
Recommendations
- The Isabelle collections framework
- Structured formal development in Isabelle
- An Isabelle proof method language
- scientific article; zbMATH DE number 65526
- scientific article; zbMATH DE number 1614689
- A consistent foundation for Isabelle/HOL
- A consistent foundation for Isabelle/HOL
- Equational reasoning in Isabelle
- Unifying theories of programming in Isabelle
- A graph library for Isabelle
Cites work
- A comparison of Mizar and Isar
- A Compiled Implementation of Normalization by Evaluation
- A formally verified proof of the prime number theorem
- Building Formal Method Tools in the Isabelle/Isar Framework
- Constructive Type Classes in Isabelle
- Context Aware Calculation and Deduction
- Edinburgh LCF. A mechanized logic of computation
- Flyspeck I: Tame Graphs
- Flyspeck II: The basic linear programs
- Formal Pervasive Verification of a Paging Mechanism
- HOLCF = HOL + LCF
- scientific article; zbMATH DE number 1629953 (Why is no real title available?)
- scientific article; zbMATH DE number 1670734 (Why is no real title available?)
- scientific article; zbMATH DE number 2003161 (Why is no real title available?)
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- scientific article; zbMATH DE number 1863378 (Why is no real title available?)
- scientific article; zbMATH DE number 1424012 (Why is no real title available?)
- Imperative Functional Programming with Isabelle/HOL
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Isabelle. A generic theorem prover
- Local Theory Specifications in Isabelle/Isar
- Logic-Free Reasoning in Isabelle/Isar
- Mechanizing the metatheory of LF
- Natural deduction as higher-order resolution
- Nominal techniques in Isabelle/HOL
- Organizing numerical theories using axiomatic type classes
- Partial Recursive Functions in Higher-Order Logic
- Set theory for verification. I: From foundations to functions
- Set theory for verification. II: Induction and recursion
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Structured formal development in Isabelle
- Structured Induction Proofs in Isabelle/Isar
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- Types for Proofs and Programs
- Types, bytes, and separation logic
Cited in
(72)- Proof assistants: history, ideas and future
- Experimenting with Isabelle in ZF set theory
- Set theory for verification. I: From foundations to functions
- Isabelle
- Aligning concepts across proof assistant libraries
- Automating formalization by statistical and semantic parsing of mathematics
- Using the Isabelle ontology framework -- linking the formal with the informal
- The foundation of a generic theorem prover
- TacticToe: learning to prove with tactics
- Machine learning guidance for connection tableaux
- Isabelle's metalogic: formalization and proof checker
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- A formalization and proof checker for Isabelle's metalogic
- The role of entropy in guiding a connection prover
- From LCF to Isabelle/HOL
- Semantics of Mizar as an Isabelle object logic
- First steps towards a formalization of forcing
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Classification of alignments between concepts of formal mathematical systems
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- scientific article; zbMATH DE number 1696609 (Why is no real title available?)
- Translating Scala programs to Isabelle/HOL. System description
- Automating free logic in Isabelle/HOL
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- An Isabelle proof method language
- Tools for the investigation of substructural and paraconsistent logics
- Proof-producing reflection for HOL. With an application to model polymorphism
- Pattern matches in HOL: a new representation and improved code generation
- Taming paraconsistent (and other) logics: an algorithmic approach
- Validating QBF Validity in HOL4
- Heterogeneous proofs: spider diagrams meet higher-order provers
- Structured formal development in Isabelle
- Building Formal Method Tools in the Isabelle/Isar Framework
- An Interpretation of Isabelle/HOL in HOL Light
- Formal Islands
- scientific article; zbMATH DE number 65526 (Why is no real title available?)
- scientific article; zbMATH DE number 1088221 (Why is no real title available?)
- scientific article; zbMATH DE number 2079996 (Why is no real title available?)
- An embedding of Ruby in Isabelle
- scientific article; zbMATH DE number 1863378 (Why is no real title available?)
- Learning-assisted theorem proving with millions of lemmas
- Superposition for bounded domains
- Formalization of Forcing in Isabelle/ZF
- Interactive theorem proving from the perspective of Isabelle/Isar
- Light-weight containers for Isabelle: efficient, extensible, nestable
- Shared-memory multiprocessing for interactive theorem proving
- An approach to the extension of a theorem prover by advanced structuring mechanisms.
- A Framework for Interactive Proof
- A Mechanized Model of the Theory of Objects
- Matching concepts across HOL libraries
- Interactive simplifier tracing and debugging in Isabelle
- The Isabelle collections framework
- Structured Induction Proofs in Isabelle/Isar
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Psi-calculi in Isabelle
- Isabelle formalisation of original representation theorems
- Isabelle/HOL/GST: a formal proof environment for generalized set theories
- Combining higher-order logic with set theory formalizations
- Verified verifying: SMT-LIB for strings in Isabelle
- Equivalence checking for orthocomplemented bisemilattices in log-linear time
- Formula normalizations in verification
- Linear resources in Isabelle/HOL
- A monadic second-order version of Tarski's geometry of solids
- Certainty in formalising SMT-LIB for strings in Isabelle
- Conway's normal form in the Mizar system
- Surreal dyadic and real numbers: a formal construction
- Surreal numbers: a study of square roots
- Learning conjecturing from scratch
- Inverse element for surreal number
- Saturating sorting without sorts
- N. G. de Bruijn's contribution to the formalization of mathematics
Describes a project that uses
Uses Software
This page was built for publication: The Isabelle Framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543647)
