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

DOI10.1007/978-3-319-43144-4_13MaRDI QIDQ2829259zbMATH OpenOpenAlexFDO

Authors Ondřej Kunčar, Andrei Popescu

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)

Recommendations

• From types to sets by local type definition in higher-order logic
• On definitions of constants and types in HOL
• A mechanized translation from higher-order logic to set theory
• A consistent foundation for Isabelle/HOL
• A consistent foundation for Isabelle/HOL

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 mechanized proof of the basic perturbation lemma
• A mechanized translation from higher-order logic to set theory
• Comprehending Isabelle/HOL’s Consistency
• Constructive Type Classes in Isabelle
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• 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
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Mechanisation of AKS algorithm. I. The main theorem
• The HOL-Omega Logic
• The Matita interactive theorem prover
• Three chapters of measure theory in Isabelle/HOL

Cited in

(7)

• Comprehending Isabelle/HOL’s Consistency
• From types to sets by local type definition in higher-order logic
• Constructing the Lie algebra of smooth vector fields on a Lie group in Isabelle/HOL
• Setoid type theory -- a syntactic translation
• Generating custom set theories with non-set structured objects
• scientific article; zbMATH DE number 1512611 (Why is no real title available?)
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting

Describes a project that uses

Uses Software

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

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

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