Quotients of Bounded Natural Functors

DOI10.1007/978-3-030-51054-1_4MaRDI QIDQ5048992zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Quotients of bounded natural functors
• Quotient categories and functors hom
• scientific article; zbMATH DE number 1145509
• Functors on the category of quasi-fibrations
• scientific article; zbMATH DE number 523065
• scientific article; zbMATH DE number 4030278
• scientific article; zbMATH DE number 5311410
• scientific article; zbMATH DE number 3953026
• scientific article; zbMATH DE number 7692247
• scientific article; zbMATH DE number 2016382

Cites work

• 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?)
• A new look at generalized rewriting in type theory
• Algebra and Coalgebra in Computer Science
• 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
• 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
• 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 by idempotent functions in Cedille
• 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
• Truly modular (co)datatypes for Isabelle/HOL
• Types and coalgebraic structure
• Unified decision procedures for regular expression equivalence

Cited in

(2)

• Linear resources in Isabelle/HOL
• scientific article; zbMATH DE number 7471712 (Why is no real title available?)

Describes a project that uses

Uses Software

• Ordinals Cardinals
• Archive Formal Proofs
• CryptHOL
• Coinductive
• Lifting
• Transfer
• Autoref
• Isabelle/HOL

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 Q5048992)