[Todos CMAT] Mañana reunión inicial del curso de Realizabilidad

[matilde en cmat.edu.uy]

Mañana miércoles a las 16 horas en el Cmat tendrá lugar la primera  
reunión del curso que dictará Alexandre Miquel, "An introduction to  
intuitionistic and classical realizability", en el marco de las  
actividades del IFUM para 2010. En la misma se hará una presentación  
del curso y se fijarán los horarios.

Este curso ha sido aprobado para el posgrado en matemática.

Copio abajo una descripción del mismo.

Saludos,

Matilde.


An introduction to intuitionistic
and classical realizability
Alexandre Miquel
Background
The Curry-Howard correspondence Proof theory was deeply renewed in
the last fifty years by the discovery of a strong correspondence between proof
theoretical concepts and the concepts of functional programming, known as
the Curry-Howard correspondence [1, 4, 2]. According to this correspondence,
each formal proof can be seen as a functional program (a.k.a. the proofs-as-
programs paradigm) that meets a specification given by the proved formula
(a.k.a. the formulæ-as-types paradigm). The study of this correspondence had
major theoretical outputs in logic, such as the discovery of type  
theory and of
linear logic. On the practical side, the Curry-Howard correspondence led to
the development of proof assistants such as Coq, MinLog, Agda, Plastic, NuPrl
(based on type theory and its variants) while influencing the design  
of functional
programming languages such as SML, Caml or Haskell.
The theory of realizability The aim of this series of lectures is to introduce
the theory of realizability [5, 9, 7], a fundamental tool to analyze  
the computa-
tional meaning of proofs through the Curry-Howard correspondence. Basically,
realizability generalizes the idea underlying standard model theory by  
interpret-
ing every formula (of a given formal system) not as a truth value 0 or 1, but
as a set of programs?thus giving 2?0 different truth values. One of the main
applications of realizability is program extraction, by which a formal  
existence
proof of a function satisfying a given specification can be turned  
into a program
that implements the corresponding function. One of the aims of these lectures
is to show how to extract such a program effectively, depending on the formal
system the source proof is formalized in.
Intuitionistic versus classical realizability Realizability was long limited
to intuitionistic logic and to constructive mathematics. In the 90?s, Krivine
developed a theory of realizability for classical logic [8], using the  
connection
between control operators (such as call/cc) and non constructive  
reasoning (such
as Peirce?s law) discovered earlier by Griffin [3]. Thanks to this  
tool, it is now
possible to extend the proofs-as-programs interpretation to classical  
mathemat-
ics (including weak forms of the axiom of choice) while keeping the  
possibility of
extracting programs from proofs. Moreover, recent work showed that classical
realizability appears to be strongly connected with Cohen?s theory of forcing
(that was introduced to prove the independence of the continuum hypothesis),
one of the main sources of inspiration of Krivine?s work.
1
Outline of the course
The series of lectures will be naturally organized in two parts. The  
first part
will be devoted to the standard presentation of realizability ? i.e.  
realizability
in intuitionistic logic ? including:
? Kleene realizability in HA (using ?-calculus and p.c.a.s)
? Formalized realizability and glued realizability
? Kreisel?s modified realizability. Practical program extraction
? Realizability in second- and higher-order Heyting arithmetic
The second part of the series of lectures will be devoted to a more advanced
topic which is the recent reformulation by Krivine of the theory of  
realizability
in the framework of classical logic, including:
? Krivine realizability. Models induced by classical realizability
? Program extraction using classical realizability
? Interpretation of the dependent axiom of choice
? Extension to higher-order arithmetic. Connections with forcing
References
[1] H. B. Curry and R. Feys. Combinatory Logic, vol. 1. North-Holland. Ams-
terdam, 1958.
[2] J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types. Cambridge Uni-
versity Press. 1989.
[3] T. Griffin. A Formulæ-as-Types Notion of Control. Principles Of Program-
ming Languages (POPL?90), 47?58. 1990.
[4] W. A. Howard. The formulae-as-types notion of construction, Privately cir-
culated notes. 1969.
[5] S. C. Kleene, On the interpretation of intuitionistic number  
theory. Journal
of Symbolic Logic, 10:109?124. 1945.
[6] G. Kreisel. Interpretation of analysis by means of functionals of  
finite type. In
A. Heyting, editor, Constructivity in Mathematics, 101?128. North-Holland,
1959.
[7] J.-L. Krivine, Lambda-calculus, types and models. Masson. 1993.
[8] J.-L. Krivine, Realizability in classical logic. In Interactive  
models of compu-
tation and program behaviour, Panoramas et synth`ses, 27:197?229. Soci ?t ?
e
ee
Math ?matique de France, 2009.
e
[9] A. S. Troelstra. Metamathematical Investigations of Intuitionistic  
Arithmetic
and Analysis. Springer, 1973. With contributions of A. S. Troelstra, C. A.
Smory ?ski, J. I. Zucker and W. A. Howard.
n
2


----------------------------------------------------------------
Centro de Matematica - www.cmat.edu.uy
Facultad de Ciencias - www.fcien.edu.uy
Universidad de la Republica - www.universidad.edu.uy

<<This message was sent using IMP, the Internet Messaging Program>>