From LCF to Isabelle/HOL

DOI10.1007/S00165-019-00492-1MaRDI QIDQ2280211zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow, Makarius Wenzel, Lawrence C. Paulson

Publication date 18 December 2019

Published in Formal Aspects of Computing (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1907.02836

zbMATH Keywords

LCFHOLinteractive theorem provingIsabelle

Mathematics Subject Classification ID

History of computer science (68-03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Interactive theorem proving from the perspective of Isabelle/Isar
• Automatic proof and disproof in Isabelle/HOL
• The Isabelle Framework
• HOL Light: An Overview
• Twenty Years of Theorem Proving for HOLs Past, Present and Future

Cites work

• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 3991418 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3714891 (Why is no real title available?)
• scientific article; zbMATH DE number 1543300 (Why is no real title available?)
• scientific article; zbMATH DE number 1552533 (Why is no real title available?)
• scientific article; zbMATH DE number 3992919 (Why is no real title available?)
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• scientific article; zbMATH DE number 2090127 (Why is no real title available?)
• scientific article; zbMATH DE number 7552936 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A Brief Overview of HOL4
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A Machine-Oriented Logic Based on the Resolution Principle
• A consistent foundation for Isabelle/HOL
• A formal proof of the Kepler conjecture
• A formally verified compiler back-end
• A framework for defining logics
• A unification algorithm for typed \(\overline\lambda\)-calculus
• A verified compiler from Isabelle/HOL to CakeML
• An implementation of hyper-resolution
• An introduction to small scale reflection in Coq
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Animating the formalised semantics of a Java-like language
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Automated Reasoning
• Automatic Data Refinement
• Automatic mode inference for logic programs
• Automatic proof and disproof in Isabelle/HOL
• Automation for interactive proof: first prototype
• CakeML
• Certification of Termination Proofs Using CeTA
• Certification of classical confluence results for left-linear term rewrite systems
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• Code generation via higher-order rewrite systems
• Combining partial-order reductions with on-the-fly model-checking.
• Combining superposition, sorts and splitting
• Computational logic: its origins and applications
• Computing in systems described by equations
• Concrete semantics. With Isabelle/HOL
• Constructive Type Classes in Isabelle
• Constructive mathematics and computer programming
• Data refinement in Isabelle/HOL
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• Edinburgh LCF. A mechanized logic of computation
• Efficient verified (UN)SAT certificate checking
• Eisbach: a proof method language for Isabelle
• Extending Sledgehammer with SMT solvers
• Fast Decision Procedures Based on Congruence Closure
• Formal verification of an executable LTL model checker with partial order reduction
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Foundational property-based testing
• Four decades of \textsc{Mizar}. Foreword
• Higher-order unification, polymorphism, and subsorts
• Imperative Functional Programming with Isabelle/HOL
• Interaction with formal mathematical documents in Isabelle/PIDE
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Isabelle as document-oriented proof assistant
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Kodkod: A Relational Model Finder
• Licensing the Mizar Mathematical Library (MML)
• Local Theory Specifications in Isabelle/Isar
• Locales: a module system for mathematical theories
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Natural deduction as higher-order resolution
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• On definitions of constants and types in HOL
• Organizing numerical theories using axiomatic type classes
• Programming with Equations
• Refinement to imperative HOL
• Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), Cork, Ireland, 2004
• Shared-memory multiprocessing for interactive theorem proving
• Smart testing of functional programs in Isabelle
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
• The Lean theorem prover (system description)
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• The foundation of a generic theorem prover
• 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
• 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
• Turning Inductive into Equational Specifications
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Uppaal in a nutshell
• Verified efficient implementation of Gabow's strongly connected component algorithm
• Verified model checking of timed automata

Cited in

(21)

• Formalizing ordinal partition relations using Isabelle/HOL
• Binary intersection formalized
• HOL Light: An Overview
• Interactive theorem proving from the perspective of Isabelle/Isar
• The Isabelle/Naproche natural language proof assistant
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Automatic proof and disproof in Isabelle/HOL
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• Population-induced phase transitions and the verification of chemical reaction networks
• Comprehending Isabelle/HOL’s Consistency
• scientific article; zbMATH DE number 2090293 (Why is no real title available?)
• Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
• Applying formal verification to an open-source real-time operating system
• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• CICM'21 systems entries
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• Twenty Years of Theorem Proving for HOLs Past, Present and Future
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• Towards mechanised proofs in double-pushout graph transformation
• Formalising the double-pushout approach to graph transformation
• A formalised theorem in the partition calculus

Describes a project that uses

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)