Kazushige TERUI (National Institute of Informatics, Tokio, Japan) sarà ospite presso l'Istituto per le Applicazioni del Calcolo dal 21 al 24 maggio pv. Durante il suo soggiorno terrà il seguente seminario:

Titolo: The use of phase semantics: to make sense out of nonsense
Speaker: Kazushige TERUI (National Institute of Informatics, Tokio, Japan)
Quando: 23/05/2007 - 11:08
Dove: Aula 12 - Facoltà Lettere e Filosofia - Università Roma Tre - Via Ostiense 234 Roma

Abstract

Phase semantics (Girard 87) and its intuitionistic/noncommutative variants (Abrusci, Okada, Sambin, Troelstra, etc.) are provability semantics for linear logic and its variants. While they are sometimes considered "abstract nonsense" (or at least uninteresting from the viewpoint of computation), one cannot deny that it has a wide range of applications. For instance:

Undecidability (Lafont)
Decidability via finite model property (Lafont, Okada-Terui, Galatos-Jipsen)
Cut-elimination (Okada, Kanovitch-Okada-Scedrov, Belardinelli-Jipsen-Ono)
Denotational completeness (Girard, Streicher)
Conservativity (Kanovitch-Okada-Terui, Hamano-Takemura)
Criteria for cut-elimination (Terui, Ciabattoni-Terui)
Interpolation and amalgamation properties (Terui)
Polarity and Focalization

Thus phase semantics is a good tool for applications, and it is still useful to study it. In this talk, I will survey some uses of phase semantics and try to extract general patterns, hoping that it will lead to more applications and establishment of phase semantics as a solid, concrete and sensible tool.