Coalgebras as Types Determined by Their Elimination Rules
From MaRDI portal
Publication:5253935
DOI10.1007/978-94-007-4435-6_16zbMath1314.68192OpenAlexW32613657MaRDI QIDQ5253935
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
