A Tutorial Workshop on Realizability Semantics and Applications
June 30-July 1, 1999

A workshop associated to the 1999 Federated Logic Conference, to be held in Trento, June 29-July 12, 1999.

Description of Workshop

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.

Tutorial Presenters

  • Ulrich Berger
  • Aurelio Carboni
  • Martin Hyland
  • Chih-Hao Luke Ong
  • Jaap van Oosten
  • Andrew M. Pitts
  • Bernhard Reus


    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

    Organizing Committee


    Bibliography on Realizability


    Maintained by:
    Lars Birkedal
    Last edited: June 14, 1999.