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
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
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- The HOL-Omega Logic
- The Matita Interactive Theorem Prover
- 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: Part 1 – 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)
