A consistent foundation for Isabelle/HOL

DOI10.1007/S10817-018-9454-8MaRDI QIDQ1739913zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• A consistent foundation for Isabelle/HOL
• Comprehending Isabelle/HOL’s Consistency
• On definitions of constants and types in HOL
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• Model-theoretic conservative extension for definitional theories

Cites work

• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A consistent foundation for Isabelle/HOL
• A mechanized translation from higher-order logic to set theory
• A new foundation for Nominal Isabelle
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• Comprehending Isabelle/HOL’s Consistency
• Constructive Type Classes in Isabelle
• First-Class Type Classes
• Foundational extensible corecursion: a proof assistant perspective
• HOL with definitions: semantics, soundness, and a verified implementation
• HOLCF = HOL + LCF
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Light-weight containers for Isabelle: efficient, extensible, nestable
• Nominal techniques in Isabelle/HOL
• Sets in Coq, Coq in Sets
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Towards Self-verification of HOL Light
• Towards a formally verified proof assistant
• Type classes and filters for mathematical analysis in Isabelle/HOL

Cited in

(21)

• Automated Deduction – CADE-20
• Isabelle/HOL/GST: a formal proof environment for generalized set theories
• A consistent foundation for Isabelle/HOL
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Isabelle's metalogic: formalization and proof checker
• On definitions of constants and types in HOL
• From LCF to Isabelle/HOL
• From types to sets by local type definition in higher-order logic
• From types to sets by local type definitions in higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Nominal techniques in Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Comprehending Isabelle/HOL’s Consistency
• scientific article; zbMATH DE number 7649970 (Why is no real title available?)
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
• A formalization and proof checker for Isabelle's metalogic
• Generating custom set theories with non-set structured objects
• HOL Zero's solutions for Pollack-inconsistency
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• The Isabelle Framework

Describes a project that uses

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

This page was built for publication: A consistent foundation for Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1739913)