From LCF to Isabelle/HOL
From MaRDI portal
Publication:2280211
DOI10.1007/s00165-019-00492-1zbMath1427.68349arXiv1907.02836OpenAlexW2971627214MaRDI QIDQ2280211
Tobias Nipkow, Makarius Wenzel, Lawrence Charles Paulson
Publication date: 18 December 2019
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1907.02836
History of computer science (68-03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
CICM'21 systems entries ⋮ Binary intersection formalized ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ A formalised theorem in the partition calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Isabelle/Naproche natural language proof assistant ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
Uses Software
- ACL2
- Coq
- Isabelle
- Nitpick
- ML
- Isabelle/HOL
- Isabelle/Isar
- VAMPIRE
- SPIN
- PVS
- Haskell
- Metis_
- Isar
- Uppaal
- Mizar
- z3
- Proof General
- HOL
- HOL Light
- CeTA
- Sledgehammer
- Kodkod
- Isabelle/PIDE
- QuickCheck
- AProVE
- LCF
- CakeML
- Coq/SSReflect
- SmallCheck
- E Theorem Prover
- Poly/ML
- Locales
- Autoref
- Eisbach
- QuickChick
- Lean
- seL4
- kepler98
- Berlekamp Zassenhaus
- CAVA LTL Modelchecker
- Gabow SCC
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Four decades of {\textsc{Mizar}}. Foreword
- On definitions of constants and types in HOL
- Eisbach: a proof method language for Isabelle
- Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), Cork, Ireland, 2004
- Formal verification of an executable LTL model checker with partial order reduction
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Combining partial-order reductions with on-the-fly model-checking.
- Computing in systems described by equations
- A unification algorithm for typed \(\overline\lambda\)-calculus
- An implementation of hyper-resolution
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Refinement to imperative HOL
- A consistent foundation for Isabelle/HOL
- Organizing numerical theories using axiomatic type classes
- Edinburgh LCF. A mechanized logic of computation
- The foundation of a generic theorem prover
- Uppaal in a nutshell
- Interaction with formal mathematical documents in Isabelle/PIDE
- A verified compiler from Isabelle/HOL to CakeML
- Verified model checking of timed automata
- Extending Sledgehammer with SMT solvers
- Locales: a module system for mathematical theories
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automation for interactive proof: first prototype
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
- A formally verified compiler back-end
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
- Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
- Smart Testing of Functional Programs in Isabelle
- Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
- Concrete Semantics
- Foundational Property-Based Testing
- Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
- Animating the Formalised Semantics of a Java-Like Language
- Automatic Proof and Disproof in Isabelle/HOL
- Turning Inductive into Equational Specifications
- Certification of Termination Proofs Using CeTA
- Constructive mathematics and computer programming
- The Lean Theorem Prover (System Description)
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Checking Conservativity of Overloaded Definitions in Higher-Order Logic
- A Brief Overview of HOL4
- Imperative Functional Programming with Isabelle/HOL
- Code Generation via Higher-Order Rewrite Systems
- Constructive Type Classes in Isabelle
- Local Theory Specifications in Isabelle/Isar
- Automatic mode inference for logic programs
- Fast Decision Procedures Based on Congruence Closure
- Programming with Equations
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A framework for defining logics
- Computational logic: its origins and applications
- Natural deduction as higher-order resolution
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- The New Quickcheck for Isabelle
- Licensing the Mizar Mathematical Library
- Isabelle as Document-Oriented Proof Assistant
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- Automated Reasoning
- Automatic Data Refinement
- Data Refinement in Isabelle/HOL
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- Shared-Memory Multiprocessing for Interactive Theorem Proving
- CakeML
- A Machine-Oriented Logic Based on the Resolution Principle
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Kodkod: A Relational Model Finder
- Higher-order unification, polymorphism, and subsorts
- Efficient verified (UN)SAT certificate checking
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
