From Types to Sets by Local Type Definitions in Higher-Order Logic

DOI10.1007/978-3-319-43144-4_13zbMath1468.68294OpenAlexW2477568018MaRDI QIDQ2829259

Andrei Popescu, Ondřej Kunčar

Publication date: 27 October 2016

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

Full work available at URL: https://eprints.mdx.ac.uk/22095/1/fromTypesToSetsITP2016update.pdf

Mathematics Subject Classification ID

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

Related Items

Generating custom set theories with non-set structured objects, A Formal Proof of the Computation of Hermite Normal Form in a General Setting, From types to sets by local type definition in higher-order logic, Comprehending Isabelle/HOL’s Consistency

Uses Software

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

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.
• A mechanized proof of the basic perturbation lemma
• Isabelle/HOL. A proof assistant for 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
• Constructive Type Classes in Isabelle
• The Matita Interactive Theorem Prover
• A Mechanized Translation from Higher-Order Logic to Set Theory