A workshop associated to the 1999 Federated Logic Conference, to be held in Trento, June 29-July 12, 1999.
There has been recently a reawaking of interest in many aspects of realizability interpretations -- especially as regards semantics of type theories for constructive reasoning and semantics of programming languages. But, the details of realizability can be quite technical, and so the aim of the workshop is to have several tutorial lectures on history, basic definitions and results, recent applications, connections to category theory, and then leave room for contributed research talks of 30 minutes each.
| Wednesday, June 30 | |
| 8.45-9.00 | Opening Dana Scott |
| 9.00-10.00 | Tripos Theory in Retrospect A. Pitts |
| 10.00-10.30 | Break |
| 10.30-11.30 | History and Developments J. van Oosten |
| 11.30-12.00 | Local Realizability Toposes and a Modal Logic for Computability S. Awodey, L. Birkedal, D.S. Scott |
| 12.00-14.00 | LUNCH |
| 14.00-15.00 | TBA J.M.E. Hyland |
| 15.00-15.30 | Matching Typed and Untyped Realizability J. Longley |
| 15.30-16.00 | Break |
| 16.00-17.30 | Completions A. Carboni |
| 17.30-18.00 | Process Realizability S. Abramsky |
| 18.00-18.30 | A Metric Model for PCF M.H. Escardo' |
| 20.00-?? | Reception |
| Thursday, July 1 | |
| 9.00-10.00 | Effectivity and Totality U. Berger |
| 10.00-10.30 | BREAK |
| 10.30-11.30 | Applications to Normalization C.-H. Luke Ong |
| 11.30-12.00 | The Uniform Provability Realization of Intuitionistic Logic, Modality
and Lambda Calculus S. Artemov |
| 12.00-14.00 | LUNCH |
| 14.00-15.00 | Realizability Semantics for Type Theories B. Reus |
| 15.00-15.30 | A Type Theory which is Complete for Kreisel's Modified Realizability T. Crolard |
| 15.30-16.00 | BREAK |
| 16.00-17.00 | Completions A. Carboni |
| 17.00-17.30 | Comparing Models of Higher Type Computation G. Rosolini, T. Streicher |