scientific article; zbMATH DE number 7649955

DOI10.4230/LIPICS.ITP.2019.6MaRDI QIDQ5875411zbMATH OpenFDO

Authors

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2019.6

zbMATH Keywords

coinductive typesdata typesinductive typespolynomial functors

Mathematics Subject Classification ID

Cites work

• A final coalgebra theorem
• A formalized hierarchy of probabilistic system types. Proof pearl
• A lattice-theoretical fixpoint theorem and its applications
• Codifying guarded definitions with recursive schemes
• Dependent inductive and coinductive types are fibrational dialgebras
• Foundational (co)datatypes and (co)recursion for higher-order logic
• Foundational nonuniform (co)datatypes for higher-order logic
• Friends with benefits. Implementing corecursion in foundational proof assistants
• scientific article; zbMATH DE number 2185663 (Why is no real title available?)
• scientific article; zbMATH DE number 42735 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1231637 (Why is no real title available?)
• scientific article; zbMATH DE number 1956503 (Why is no real title available?)
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Indexed containers
• Inductive families
• Isabelle/HOL. A proof assistant for higher-order logic
• Mathematics of Program Construction
• On tree coalgebras and coalgebra presentations
• Pragmatic quotient types in Coq
• Relating coalgebraic notions of bisimulation. With applications to name-passing process calculi (extended abstract)
• Relation lifting, a survey
• Terminal coalgebras in well-founded set theory
• The Lean theorem prover (system description)
• Theorem Proving in Higher Order Logics
• Truly modular (co)datatypes for Isabelle/HOL
• Type theory based on dependent inductive and coinductive types
• Types for Proofs and Programs
• Une théorie combinatoire des séries formelles
• Universal coalgebra: A theory of systems

Cited in

(5)

• Non-well-founded deduction for induction and coinduction
• Quotients of bounded natural functors
• Quotients of Bounded Natural Functors
• Polynomial Functors and Shannon Entropy
• Formalising inductive and coinductive containers

Describes a project that uses

Uses Software

• AmiCo
• Lean
• Isabelle/HOL
• Zoo Probabilistic Systems

This page was built for publication:

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