Integrating Linear and Dependent Types.
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 12099
- Type
- E - Conference contribution
- DOI
-
10.1145/2775051.2676969
- Title of conference / published proceedings
- POPL
- First page
- 17
- Volume
- -
- Issue
- -
- ISSN
- 0362-1340
- Open access status
- Out of scope for open access requirements
- Month of publication
- -
- Year of publication
- 2015
- 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
- 2
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper gave one of the first descriptions of a syntax for dependent type theory augmented with linear types, with an eye toward verification of simple imperative programs. As such, it is cited by several subsequent works using the combination of linear and dependent types towards various ends, including quantum programming (https://doi.org/10.1145/3009837.3009894) and effect systems (doi:10.1007/978-3-662-49630-5\_3), among others; more foundational developments include (https://doi.org/10.1007/978-3-319-30936-1_22) and (https://doi.org/10.1145/3209108.3209189). It was also used as a basis for a course at the Oregon Programming Language Summer School (https://www.youtube.com/watch?v=5i3YDgQyIwE). A prototype type-checker was submitted with the paper and is available online (https://dl.acm.org/doi/pdf/10.1145/2676726.2676969).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -