Undecidability of equality for codata types

DOI10.1007/978-3-030-00389-0_4OpenAlexW2883066834MaRDI QIDQ1798783

Anton Setzer, Ulrich Berger

Publication date: 23 October 2018

Full work available at URL: https://cronfa.swan.ac.uk/Record/cronfa38822/Download/0038822-28022018014103.pdf

zbMATH Keywords

coalgebrapattern matchingMartin-Löf type theoryundecidability resultsinseparabilitydependent type theoryintensional type theorycodatacopattern matchingdecidable type checkingintensional equalityweakly final coalgebras

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Intuitionistic fixed point logic

Uses Software

• Coq
• Agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Codatatypes in ML
• Classical recursion theory. The theory of functions and sets of natural numbers.
• Universal coalgebra: A theory of systems
• Inductive types and type constraints in the second-order lambda calculus
• Inductive, coinductive, and pointed types
• Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)
• Copatterns
• How to Reason Coinductively Informally
• ΠΣ: Dependent Types without the Sugar
• Subtyping, Declaratively
• Type Theory based on Dependent Inductive and Coinductive Types
• Coalgebras as Types Determined by Their Elimination Rules
• Interactive programming in Agda – Objects and graphical user interfaces
• Extensions of some theorems of Gödel and Church
• Infinite objects in type theory
• Codifying guarded definitions with recursive schemes