Program of the Workshop

Lectures

• Jean-Louis Krivine: realizing the ultrafilter on N. (homepage)

Invited Talks

• Thierry Coquand: (homepage)
  • A semantics of evidence for classical arithmetics
  • Forcing and type theory

• Paulo Oliva: Realizability Interpretations of Linear Logic (homepage)
  • Abstract: in this talk I will present realizability interpretations of both classical (LL) and intuitionistic linear logic (ILL) [1,2]. Viewing linear logic as a refinement of intuitionistic logic (IL), we show how the realizability interpretations of linear logic can be thought of as a refinement of the standard modified realizability of IL (via Girard's embedding of IL into ILL). We will also look at how realizability compares to other functional interpretations (mainly, Dialectica and Diller-Nahm interpretations) in the ILL setting [3]. Finally, we show how all interpretations can be combined into a "hybrid" interpretation of a multi-modal extension of ILL [4, 5].
  • References:
    • [1] Modified realizability interpretation of classical linear logic, LICS 2007.
    • [2] Functional interpretations of intuitionistic linear logic, with G. Ferreira, in preparation.
    • [3] Functional interpretations of linear and intuitionistic logic, to appear in: I&C.
    • [4] Hybrid functional interpretations, with M.-D. Hernest, CiE 2008 (LNCS 5028:251-260, 2008)
    • [5] Hybrid functional interpretations of linear and intuitionistic logic, to appear in: JoL&C

Schedule

The workshop will officially start on Tuesday the 2nd of June, at 9'00 a.m. Everything will take place in "amphithéatre 4-Canton" (building 10 in red on this map).

Tuesday the 2nd, morning

• 9'00 — 10'00: coffee, arrival, etc.
• 10'00 — 12'00: Jean-Louis Krivine, course 1.

Tuesday the 2nd,afternoon

• 14'00 — 17'00: Jean-Louis Krivine, course 2.

Wednesday the 3rd, morning

• 9'00 — 12'00: invited speaker: Paulo Oliva, Realizability Interpretations of Linear Logic

Wednesday the 3rd,afternoon

• 14'00 — 17'00: Jean-Louis Krivine, course 3.

Thursday the 4th, morning

• 9'00 — 12'00: contributed talks.
  • Alexandre Miquel: Classical Realizability with Forcing
  • Jonas Frey: A universal characterization of the tripos to topos construction (Slides)
  • Guillaume Munch-Maccagnoni: Classical realizability and focalization (Slides)

Thursday the 4th, afternoon

• 14'00 — 17'00: Jean-Louis Krivine, course 4.

Friday the 5th, morning

• 9'00 — 12'00: invited speaker: Thierry Coquand: "a semantics of evidence for classical arithmetics" (Slides) and "forcing and type theory" (Slides).

Friday the 5th, afternoon

• 14'00 — 16'30: contributed talks.
  • Paul-André Mellies: (cancelled)
  • Jaime Gaspar: Proof interpretations with truth (Slides)
  • Christophe Raffalli: Realizability for programming languages

Social Events

• Wednesday evening: barbecue at the "Plage de Motets"
• Thursday evening: restaurant "Les Momes" in Chambéry