A consistent foundation for Isabelle/HOL

DOI10.1007/s10817-018-9454-8zbMath1465.68289OpenAlexW3023928742MaRDI QIDQ1739913

Ondřej Kunčar, Andrei Popescu

Publication date: 29 April 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

consistencytheorem provinghigher-order logicIsabelle/HOLmodel-theoretic semanticsad hoc overloading

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

ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT ⋮ Generating custom set theories with non-set structured objects ⋮ Isabelle/HOL/GST: a formal proof environment for generalized set theories ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ From LCF to Isabelle/HOL ⋮ Isabelle's metalogic: formalization and proof checker ⋮ A formalization and proof checker for Isabelle's metalogic

Uses Software

• Coq
• Isabelle
• ML
• Isabelle/HOL
• Isabelle/Isar
• Isar
• Mizar
• HOL
• ProofPower
• HOL Light
• Agda
• Milawa
• Nominal Isabelle
• Jitawa
• HOL Zero
• Light-weight Containers

Cites Work

• Unnamed Item
• 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
• A Consistent Foundation for Isabelle/HOL
• Foundational extensible corecursion: a proof assistant perspective
• Comprehending Isabelle/HOL’s Consistency
• 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
• A Mechanized Translation from Higher-Order Logic to Set Theory