Quotients of bounded natural functors

MaRDI QIDQ5028480zbMATH OpenFDO

Authors Basil Fürer, Joshua Schneider, Dmitriy Traytel, Andreas Lochbihler

Publication date 9 February 2022

Full work available at URL https://arxiv.org/abs/2104.05348, https://lmcs.episciences.org/9022

zbMATH Keywords

functorshigher-order logicinductive and coinductive datatypesproof assistantsquotient types

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Quotients of Bounded Natural Functors
• Relational parametricity and quotient preservation for modular (co)datatypes
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 2003152

Cites work

• A new look at generalized rewriting in type theory
• Algebra and Coalgebra in Computer Science
• Almost event-rate independent monitoring
• Automatic refinement to efficient data structures: a comparison of two approaches
• Cardinals in Isabelle/HOL
• Concrete semantics. With Isabelle/HOL
• CryptHOL: game-based proofs in higher-order logic
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Defining functions on equivalence classes
• Effect polymorphism in higher-order logic (proof pearl)
• Equational Reasoning with Applicative Functors
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• From types to sets by local type definition in higher-order logic
• General bindings and alpha-equivalence in Nominal Isabelle
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 2003152 (Why is no real title available?)
• scientific article; zbMATH DE number 1927427 (Why is no real title available?)
• scientific article; zbMATH DE number 3291978 (Why is no real title available?)
• scientific article; zbMATH DE number 3367098 (Why is no real title available?)
• scientific article; zbMATH DE number 7649955 (Why is no real title available?)
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Mathematics of Program Construction
• Pragmatic quotient types in Coq
• Presentation of set functors: a coalgebraic perspective
• Quotients of Bounded Natural Functors
• Refinements for free!
• Relational parametricity and quotient preservation for modular (co)datatypes
• Terminal coalgebras in well-founded set theory
• Theorem Proving in Higher Order Logics
• Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor.
• Types and coalgebraic structure
• Unified decision procedures for regular expression equivalence
• Witnessing (co)datatypes

Cited in

(1)

• Quotients of Bounded Natural Functors

Describes a project that uses

Uses Software

• Regex_Equivalence
• Cubical Agda
• Isabelle/HOL
• Autoref
• Transfer
• Lifting
• CryptHOL
• Monomorphic Monad

This page was built for publication: Quotients of bounded natural functors

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