Notions of anonymous existence in Martin-Löf type theory
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 43007213
- Type
- D - Journal article
- DOI
-
10.23638/LMCS-13(1:15)2017
- Title of journal
- Logical Methods in Computer Science
- Article number
- 15
- First page
- 1
- Volume
- 13
- Issue
- 1
- ISSN
- 1860-5974
- Open access status
- Compliant
- 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
-
3
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Homotopy Type Theory, or Univalent Foundations, relies on a logic that combines the Curry-Howard correspondence with a new notion of proposition proposed by Voevodsky. This paper develops this new logic with a number of fundamental new results, which are already being applied by the community. The results are implemented in the various HoTT/UF libraries in the proof assistants Coq, Agda and Lean. We have also been invited by Andrew Pitts to present this at the Newton Institute in Cambridge at the programme "Big Proof". https://www.newton.ac.uk/event/bpr
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
