Quotients of Bounded Natural Functors

DOI10.1007/978-3-030-51054-1_4OpenAlexW3038972565MaRDI QIDQ5048992FDOQ5048992

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

Recommendations

• scientific article; zbMATH DE number 7471712
• 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
• scientific article; zbMATH DE number 3953026
• scientific article; zbMATH DE number 7692247
• scientific article; zbMATH DE number 2016382

Mathematics Subject Classification ID

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

Cites Work

• Unified Decision Procedures for Regular Expression Equivalence
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Concrete Semantics
• Title not available (Why is that?)
• Terminal coalgebras in well-founded set theory
• Title not available (Why is that?)
• Refinements for Free!
• Types and coalgebraic structure
• Algebra and Coalgebra in Computer Science
• Title not available (Why is that?)
• Truly Modular (Co)datatypes for Isabelle/HOL
• Presentation of Set Functors: A Coalgebraic Perspective
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• Defining functions on equivalence classes
• Pragmatic Quotient Types in Coq
• Cardinals in Isabelle/HOL
• 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
• Relational parametricity and quotient preservation for modular (co)datatypes
• CryptHOL: game-based proofs in higher-order logic
• Equational Reasoning with Applicative Functors
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic refinement to efficient data structures: a comparison of two approaches
• Mathematics of Program Construction
• Quotients by Idempotent Functions in Cedille
• Effect polymorphism in higher-order logic (proof pearl)

Cited In (2)

• Linear resources in Isabelle/HOL
• Title not available (Why is that?)

Uses Software

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

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)