Coalgebras as Types Determined by Their Elimination Rules

DOI10.1007/978-94-007-4435-6_16zbMath1314.68192OpenAlexW32613657MaRDI QIDQ5253935

Anton Setzer

Publication date: 5 June 2015

Published in: Epistemology versus Ontology (Search for Journal in Brave)

Full work available at URL: https://cronfa.swan.ac.uk/Record/cronfa19415/Download/0019415-17052015172846.pdf

Mathematics Subject Classification ID

Related Items (3)

Interactive programming in Agda – Objects and graphical user interfaces ⋮ How to Reason Coinductively Informally ⋮ Undecidability of equality for codata types

Cites Work

• Strong categorical datatypes II: A term logic for categorical programming
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Constructions, proofs and the meaning of logical constants
• Codatatypes in ML
• Categorical logic and type theory
• Induction-recursion and initial algebras.
• Five observations concerning the intended meaning of the intuitionistic logical constants
• Indexed induction-recursion
• Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)
• A fixedpoint approach to implementing (Co)inductive definitions
• Contextual modal type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Coalgebras as Types Determined by Their Elimination Rules