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

matilde en cmat.edu.uy matilde en cmat.edu.uy
Mar Nov 23 16:42:23 UYST 2010

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.

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
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 , using the
connection
between control operators (such as call/cc) and non constructive
reasoning (such
as Peirce?s law) discovered earlier by Griffin . 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
 H. B. Curry and R. Feys. Combinatory Logic, vol. 1. North-Holland. Ams-
terdam, 1958.
 J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types. Cambridge Uni-
versity Press. 1989.
 T. Griffin. A Formulæ-as-Types Notion of Control. Principles Of Program-
ming Languages (POPL?90), 47?58. 1990.
 W. A. Howard. The formulae-as-types notion of construction, Privately cir-
culated notes. 1969.
 S. C. Kleene, On the interpretation of intuitionistic number
theory. Journal
of Symbolic Logic, 10:109?124. 1945.
 G. Kreisel. Interpretation of analysis by means of functionals of
finite type. In
A. Heyting, editor, Constructivity in Mathematics, 101?128. North-Holland,
1959.
 J.-L. Krivine, Lambda-calculus, types and models. Masson. 1993.
 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
 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