Comprehending Isabelle/HOL’s Consistency

DOI10.1007/978-3-662-54434-1_27zbMath1485.68285OpenAlexW2596784831MaRDI QIDQ2988665

Ondřej Kunčar, Andrei Popescu

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/22097/1/compr_IsabelleHOL_consupdate.pdf

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

CryptHOL: game-based proofs in higher-order logic, From types to sets by local type definition in higher-order logic, 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, From Types to Sets by Local Type Definitions in Higher-Order Logic, Model-theoretic conservative extension for definitional theories, Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL, A formalization and proof checker for Isabelle's metalogic

Uses Software

• Coq
• Isabelle
• ML
• Isabelle/HOL
• Isabelle/Isar
• Isar
• HOL
• HOL Light
• HOL-Omega
• seL4
• Berlekamp Zassenhaus
• Perron Frobenius
• Archive Formal Proofs
• CAVA LTL Modelchecker

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On definitions of constants and types in HOL
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Proof assistants: history, ideas and future
• Isabelle/HOL. A proof assistant for higher-order logic
• A consistent foundation for Isabelle/HOL
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• From Types to Sets by Local Type Definitions in Higher-Order Logic
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• Concrete Semantics
• Proof-Producing Reflection for HOL
• A Consistent Foundation for Isabelle/HOL
• Foundational extensible corecursion: a proof assistant perspective
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Comprehending Isabelle/HOL’s Consistency
• HOL Light: An Overview
• The HOL-Omega Logic
• Checking Conservativity of Overloaded Definitions in Higher-Order Logic
• Imperative Functional Programming with Isabelle/HOL
• Verifying a Compiler for Java Threads
• Code Generation via Higher-Order Rewrite Systems