From LCF to Isabelle/HOL
From MaRDI portal
Publication:2280211
DOI10.1007/S00165-019-00492-1zbMATH Open1427.68349arXiv1907.02836OpenAlexW2971627214MaRDI QIDQ2280211FDOQ2280211
Authors: Tobias Nipkow, Makarius Wenzel, Lawrence C. Paulson 
Publication date: 18 December 2019
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Abstract: Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing techniques from the world of first order theorem proving, but also the automatic search for counterexamples. They include a highly readable structured language of proofs and a unique interactive development environment for editing live proof documents. Everything rests on the foundation conceived by Robin Milner for Edinburgh LCF: a proof kernel, using abstract types to ensure soundness and eliminate the need to store proofs. Compared with the research prototypes of the 1970s, Isabelle is a practical and versatile tool. It is used by system designers, mathematicians and many others.
Full work available at URL: https://arxiv.org/abs/1907.02836
Recommendations
History of computer science (68-03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Uppaal in a nutshell
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automatic proof and disproof in Isabelle/HOL
- Certification of Termination Proofs Using CeTA
- A Brief Overview of HOL4
- Title not available (Why is that?)
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Kodkod: A Relational Model Finder
- Edinburgh LCF. A mechanized logic of computation
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Foundational property-based testing
- The Lean theorem prover (system description)
- Automated Reasoning
- Automatic Data Refinement
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- A framework for defining logics
- Type classes and filters for mathematical analysis in Isabelle/HOL
- A Machine-Oriented Logic Based on the Resolution Principle
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Extending Sledgehammer with SMT solvers
- Locales: a module system for mathematical theories
- Combining superposition, sorts and splitting
- Four decades of \textsc{Mizar}. Foreword
- On definitions of constants and types in HOL
- Eisbach: a proof method language for Isabelle
- Concrete semantics. With Isabelle/HOL
- An introduction to small scale reflection in Coq
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- Licensing the Mizar Mathematical Library (MML)
- Isabelle as document-oriented proof assistant
- Shared-memory multiprocessing for interactive theorem proving
- CakeML
- Combining partial-order reductions with on-the-fly model-checking.
- Fast Decision Procedures Based on Congruence Closure
- Animating the formalised semantics of a Java-like language
- Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), Cork, Ireland, 2004
- Constructive Type Classes in Isabelle
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formally verified compiler back-end
- Code generation via higher-order rewrite systems
- Computing in systems described by equations
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Imperative Functional Programming with Isabelle/HOL
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Automation for interactive proof: first prototype
- Natural deduction as higher-order resolution
- Local Theory Specifications in Isabelle/Isar
- The foundation of a generic theorem prover
- A verified compiler from Isabelle/HOL to CakeML
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Efficient verified (UN)SAT certificate checking
- Programming with Equations
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Higher-order unification, polymorphism, and subsorts
- Formal verification of an executable LTL model checker with partial order reduction
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Data refinement in Isabelle/HOL
- Constructive mathematics and computer programming
- Verified model checking of timed automata
- An implementation of hyper-resolution
- Automatic mode inference for logic programs
- Title not available (Why is that?)
- A formal proof of the Kepler conjecture
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
- A consistent foundation for Isabelle/HOL
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Refinement to imperative HOL
- Checking Conservativity of Overloaded Definitions in Higher-Order Logic
- Organizing numerical theories using axiomatic type classes
- Title not available (Why is that?)
- Turning Inductive into Equational Specifications
- Interaction with formal mathematical documents in Isabelle/PIDE
- Computational logic: its origins and applications
- Smart testing of functional programs in Isabelle
- Certification of classical confluence results for left-linear term rewrite systems
- Asynchronous user interaction and tool integration in Isabelle/PIDE
- Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
- Title not available (Why is that?)
Cited In (21)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Title not available (Why is that?)
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Title not available (Why is that?)
- CICM'21 systems entries
- Title not available (Why is that?)
- Title not available (Why is that?)
- Binary intersection formalized
- A formalised theorem in the partition calculus
- Formalising the double-pushout approach to graph transformation
- Interactive theorem proving from the perspective of Isabelle/Isar
- Lessons learned from LCF: A Survey of Natural Deduction Proofs
- The Isabelle/Naproche natural language proof assistant
- Formalizing Ordinal Partition Relations Using Isabelle/HOL
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Automatic proof and disproof in Isabelle/HOL
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- Applying formal verification to an open-source real-time operating system
- HOL Light: An Overview
- Comprehending Isabelle/HOL’s Consistency
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
This page was built for publication: From LCF to Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2280211)
