How to Reason Coinductively Informally

DOI10.1007/978-3-319-29198-7_12zbMath1439.03071OpenAlexW2470575749MaRDI QIDQ3305562

Anton Setzer

Publication date: 7 August 2020

Published in: Advances in Proof Theory (Search for Journal in Brave)

Full work available at URL: https://cronfa.swan.ac.uk/Record/cronfa24566

Mathematics Subject Classification ID

Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65) Foundations, relations to logic and deductive systems (18A15) Type theory (03B38)

Related Items

Interactive programming in Agda – Objects and graphical user interfaces ⋮ Undecidability of equality for codata types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Calculi for synchrony and asynchrony
• Induction-recursion and initial algebras.
• Universal coalgebra: A theory of systems
• Terminal coalgebras in well-founded set theory
• Indexed induction-recursion
• Copatterns
• Introduction to Bisimulation and Coinduction
• A set constructor for inductive sets in Martin-Löf's type theory
• A final coalgebra theorem
• Wellfounded recursion with copatterns
• Coalgebras as Types Determined by Their Elimination Rules
• Small Induction Recursion
• Indexed containers

This page was built for publication: How to Reason Coinductively Informally