Quotients of Bounded Natural Functors

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

Mathematics Subject Classification ID

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

Related Items (1)

Unnamed Item

Uses Software

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

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