Partiality, revisited: the partiality monad as a quotient inductive-inductive type
- Submitting institution
-
University of Nottingham, The
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1330108
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-662-54458-7_31
- Title of conference / published proceedings
- Foundations of Software Science and Computation Structures: FoSSaCS 2017
- First page
- 534
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- March
- Year of publication
- 2017
- 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
-
2
- Research group(s)
-
-
- Citation count
- 6
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper solved a long-standing open problem, namely how to define the partiality monad in type theory without using the axiom of choice. We use novel concepts from Homotopy Type Theory, namely Higher Inductive Types, to address this issue. The result enables us to create a connection with classical results in domain theory (we construct the free omega DCPO) and has important practical applications when combining total and partial programming in the context of type theory. Ideas from this paper have been used in related projects, e.g. by people working with the COQ system.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
