Quotients of Bounded Natural Functors
From MaRDI portal
Publication:5048992
DOI10.1007/978-3-030-51054-1_4OpenAlexW3038972565MaRDI QIDQ5048992
Basil Fürer, Joshua Schneider, Dmitriy Traytel, Andreas Lochbihler
Publication date: 9 November 2022
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_4
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- From types to sets by local type definition in higher-order logic
- Relational parametricity and quotient preservation for modular (co)datatypes
- CryptHOL: game-based proofs in higher-order logic
- Terminal coalgebras in well-founded set theory
- Automatic refinement to efficient data structures: a comparison of two approaches
- Types and coalgebraic structure
- Equational Reasoning with Applicative Functors
- Truly Modular (Co)datatypes for Isabelle/HOL
- Cardinals in Isabelle/HOL
- Unified Decision Procedures for Regular Expression Equivalence
- Concrete Semantics
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Refinements for Free!
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Presentation of Set Functors: A Coalgebraic Perspective
- Quotients by Idempotent Functions in Cedille
- Defining functions on equivalence classes
- Mathematics of Program Construction
- Pragmatic Quotient Types in Coq
- Theorem Proving in Higher Order Logics
- Algebra and Coalgebra in Computer Science
- Effect polymorphism in higher-order logic (proof pearl)
This page was built for publication: Quotients of Bounded Natural Functors