The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 24112354
- Type
- E - Conference contribution
- DOI
-
10.4230/LIPIcs.TLCA.2015.153
- Title of conference / published proceedings
- 13th International Conference on Typed Lambda Calculi and Applications, Proceedings
- First page
- 153
- Volume
- 38
- Issue
- -
- ISSN
- 1868-8969
- Open access status
- Out of scope for open access requirements
- Month of publication
- July
- 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
-
1
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Computable functions are known to be continuous, which goes back Brouwer in the 1920's. Intensional Martin-Löf type theory (MLTT) is the foundation of many proof assistants for constructive mathematics and homotopy type theory. It was tacitly assumed by the research community that the principle "all functions are continuous" is compatible with MLTT due to the fact that MLTT is based on the Brouwer-Heyting-Kolmogorov-Curry-Howard interpretation of constructive logic. However, we show this principle is not only incompatible with MLTT but also provably false. We were invited by Martin-Löf and Maietti to present this work at the Institut Mittag-Leffler, Stockholm. http://www.mittag-leffler.se/workshop/fifth-workshop-formal-topology-spreads-and-choice-sequences.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -