From types to sets by local type definition in higher-order logic

DOI10.1007/s10817-018-9464-6zbMath1468.68295OpenAlexW2806477068MaRDI QIDQ1722645

Andrei Popescu, Ondřej Kunčar

Publication date: 18 February 2019

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

Full work available at URL: https://doi.org/10.1007/s10817-018-9464-6

zbMATH Keywords

consistencytransferrelativizationdependent typesHOLIsabelleoverloadingtype classestype definitionlocal typedefset-based theoremstype-based theorems

Mathematics Subject Classification ID

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

Related Items (11)

Quotients of Bounded Natural Functors ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ Combining higher-order logic with set theory formalizations ⋮ A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL ⋮ Unnamed Item ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory ⋮ A formalization of the Smith normal form in higher-order logic

Uses Software

• Coq
• Isabelle
• ML
• Isabelle/HOL
• Mizar
• HOL
• Matita
• HOL Light
• HOL-Omega
• Nuprl
• Agda
• Locales
• HOL Zero
• Transfer
• Lifting
• Berlekamp Zassenhaus

Cites Work

• Unnamed Item
• A formalization of metric spaces in HOL Light
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A mechanized proof of the basic perturbation lemma
• Isabelle/HOL. A proof assistant for higher-order logic
• The HOL Light theory of Euclidean space
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Locales: a module system for mathematical theories
• From Types to Sets by Local Type Definitions in Higher-Order Logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Comprehending Isabelle/HOL’s Consistency
• Three Chapters of Measure Theory in Isabelle/HOL
• A Brief Overview of Agda – A Functional Language with Dependent Types
• The HOL-Omega Logic
• Mizar: State-of-the-art and Beyond
• Constructive Type Classes in Isabelle
• The Matita Interactive Theorem Prover
• Theorem Proving in Higher Order Logics
• A Mechanized Translation from Higher-Order Logic to Set Theory

This page was built for publication: From types to sets by local type definition in higher-order logic