Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Special Session Talk:
Krivine's realizability: from storage operators to the intentional axiom of choice

Edit abstract data

Speaker: Christophe Raffalli


We will give a survey of some results in realizability including:

  • basic notions and control operators associated to Pierce's law.
  • the definition of data-types and storage operators (which are essential).
  • the interaction of intuitionistic and classical proofs to extract algorithm (illustrated by Dickson's lemma).
  • the use of the system clock to realize the intentional axiom of choice.
  • We will also give a short list of open problems.

websites: Arnold Beckmann 2007-11-12 Valid HTML 4.01! Valid CSS!