Control operators as constructive extensions of intuitionistic logic
Speaker: Danko Ilik
Venue: Salle Philippe Flajolet, LIX, Alan Turing Building
Date: 19 March 2013, 13h30
Since the observations of Felleisen and Griffin, in the early 1990s,
that control operators from the theory of programming languages can be
used to extend the Curry-Howard correspondence from intuitionistic to
classical logic, these operators (and, by extrapolation, computational
side-effects) have been taught of as non-constructive. Yet, in recent
works of Herbelin and the author, it has been shown that constructive
logical systems, weaker than classical logic, and stronger than
intuitionistic logic, can be built using them.
In this talk, I will survey these systems and discuss some of their
recent applications and meta-mathematical implications, like the
provability of Open Induction on Cantor space, or the status of the
arithmetical Church’s Thesis.
