Undecidability of Equality for Codata Types
- Submitting institution
-
Swansea University / Prifysgol Abertawe
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 38822
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-030-00389-0_4
- Title of conference / published proceedings
- Coalgebraic Methods in Computer Science
- First page
- 34
- Volume
- 11202
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- September
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Dependent type theory allows to define generic programs in functional programming. Codata types is the main approach in functional programming for representing non-terminating processes. However, here is the first proof that type checking for codata types in dependent type theory is algorithmically undecidable; therefore, programmers need to do extra work to manually type check programs. Based on the results of this paper, codata types have been replaced by the alternative approach of coalgebras in the dependently typed programming language and theorem prover Agda. Object-oriented programs and GUIs in Agda have been developed using this approach.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -