The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
Martín Escardó and Chuangjie Xu.
- The paper. Last updated 15th April 2015 taking referees' comments into account. This is the submitted final version.
-
- Agda version of Section 2 of the paper, without identity types (and with identity types).
-
- Agda version of Section 4 of the paper.
-
- zip file with all the Agda files.
-
- Slides for the IHP 2014 talk and
slides for the Mittag-Leffler 2015 talk.
and slides for the TLCA'2015 talk.
-
Last modified Thu 14 June 2015 20:26 BST