The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation

Martín Escardó and Chuangjie Xu.


  1. The paper. Last updated 15th April 2015 taking referees' comments into account. This is the submitted final version.

  2. Agda version of Section 2 of the paper, without identity types (and with identity types).

  3. Agda version of Section 4 of the paper.

  4. zip file with all the Agda files.

  5. 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