Undecidability of equality for codata types
From MaRDI portal
Publication:1798783
DOI10.1007/978-3-030-00389-0_4OpenAlexW2883066834MaRDI QIDQ1798783
Publication date: 23 October 2018
Full work available at URL: https://cronfa.swan.ac.uk/Record/cronfa38822/Download/0038822-28022018014103.pdf
coalgebrapattern matchingMartin-Löf type theoryundecidability resultsinseparabilitydependent type theoryintensional type theorycodatacopattern matchingdecidable type checkingintensional equalityweakly final coalgebras
Related Items
Uses Software
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
