A Consistent Foundation for Isabelle/HOL

DOI10.1007/978-3-319-22102-1_16zbMath1433.68556OpenAlexW2791394679MaRDI QIDQ2945636

Ondřej Kunčar, Andrei Popescu

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/16073/1/isabelleHOL.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (13)

Automating change of representation for proofs in discrete mathematics (extended version) ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Formalising Mathematics in Simple Type Theory ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ A consistent foundation for Isabelle/HOL ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ Isabelle's metalogic: formalization and proof checker ⋮ A formally verified abstract account of Gödel's incompleteness theorems ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Model-theoretic conservative extension for definitional theories ⋮ A formalization and proof checker for Isabelle's metalogic

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• PVS
• HOL
• ProofPower
• HOL Light
• Agda

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Nominal techniques in Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Towards a Formally Verified Proof Assistant
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• The Reflective Milawa Theorem Prover Is Sound
• Concrete Semantics
• A Consistent Foundation for Isabelle/HOL
• Foundational extensible corecursion: a proof assistant perspective
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• First-Class Type Classes
• Constructive Type Classes in Isabelle
• Towards Self-verification of HOL Light
• HOLCF = HOL + LCF
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• A New Foundation for Nominal Isabelle

This page was built for publication: A Consistent Foundation for Isabelle/HOL