From types to sets by local type definitions in higher-order logic
From MaRDI portal
Publication:2829259
DOI10.1007/978-3-319-43144-4_13zbMATH Open1468.68294OpenAlexW2477568018MaRDI QIDQ2829259FDOQ2829259
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
Recommendations
Cites Work
- Title not available (Why is that?)
- The HOL-Omega Logic
- The Matita interactive theorem prover
- Title not available (Why is that?)
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A mechanized translation from higher-order logic to set theory
- Three chapters of measure theory in Isabelle/HOL
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Constructive Type Classes in Isabelle
- A mechanized proof of the basic perturbation lemma
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Mechanisation of AKS algorithm. I. The main theorem
- Comprehending Isabelle/HOL’s Consistency
Cited In (6)
- From types to sets by local type definition in higher-order logic
- Setoid type theory -- a syntactic translation
- Generating custom set theories with non-set structured objects
- Title not available (Why is that?)
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- Comprehending Isabelle/HOL’s Consistency
Uses Software
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)
