Undecidability of equality for codata types
From MaRDI portal
coalgebrapattern matching[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=Martin-L%EF%BF%BD%EF%BF%BDf+type+theory&go=Go Martin-L��f type theory]undecidability resultsinseparabilitydependent type theoryintensional type theorycodatacopattern matchingdecidable type checkingintensional equalityweakly final coalgebras
Recommendations
- Type sharing constraints and undecidability
- Unsolvability of type correctness problem for functional programs
- Type inhabitation of atomic polymorphism is undecidable
- Wild representation type and undecidability
- Irrelevance, heterogeneous equality, and call-by-value dependent type systems
- Irrelevance in type theory with a heterogeneous equality judgement
- On the equivalence of types
- The underdetermination of typings
- Typability and type checking in System F are equivalent and undecidable
- scientific article; zbMATH DE number 445160
Cites work
- scientific article; zbMATH DE number 1670486 (Why is no real title available?)
- scientific article; zbMATH DE number 4047683 (Why is no real title available?)
- scientific article; zbMATH DE number 1303203 (Why is no real title available?)
- scientific article; zbMATH DE number 1064116 (Why is no real title available?)
- scientific article; zbMATH DE number 1956503 (Why is no real title available?)
- scientific article; zbMATH DE number 2247254 (Why is no real title available?)
- scientific article; zbMATH DE number 3057484 (Why is no real title available?)
- scientific article; zbMATH DE number 3078481 (Why is no real title available?)
- Classical recursion theory. The theory of functions and sets of natural numbers.
- Coalgebras as types determined by their elimination rules
- Codatatypes in ML
- Codifying guarded definitions with recursive schemes
- Copatterns, programming infinite structures by observations
- Extensions of some theorems of Gödel and Church
- Functional programming with apomorphisms (corecursion)
- How to reason coinductively informally
- Inductive types and type constraints in the second-order lambda calculus
- Inductive, coinductive, and pointed types
- Infinite objects in type theory
- Interactive programming in Agda -- objects and graphical user interfaces
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
- Subtyping, declaratively. An exercise in mixed induction and coinduction
- Type theory based on dependent inductive and coinductive types
- Universal coalgebra: A theory of systems
- \(\Pi \Sigma \): dependent types without the sugar
Cited in
(2)
This page was built for publication: Undecidability of equality for codata types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1798783)
