Peter Dybjer
Professor of Computer Science-Chalmers University of Technology, Gothenburg, Sweden

Game Semantics and Normalization by Evaluation

Game semantics and normalization by evaluation have both been active fields of research since the 1990s. In game semantics computation a program is thought of as a player playing a game against the enviroment. Among other things game semantics has been proposed as a solution to the long standing full abstraction problem in semantics. Normalization by evaluation on the other hand is a technique for computing normal forms in lambda calculi by interpreting terms in a model and then "reifying" the result. We shall here show a new way to present Hyland and Ong's game semantics for PCF by using normalization by evaluation (nbe). We use the bijective correspondence between innocent well-bracketed strategies and PCF Bohm trees, and show how operations on PCF Bohm trees, such as composition, can be computed lazily and simply by nbe. The usual equations characteristic of games follow from the nbe construction without reference to low-level game-theoretic machinery. As an illustration, we give a Haskell program computing the application of innocent strategies. (joint work with Pierre Clairambault, CNRS, ENS Lyon).

Peter Dybjer is a professor of Computer Science at Chalmers University of Technology, Gothenburg, Sweden. His main field of interest is Martin-Löf's intuitionistic type theory. Among other things he has developed the theory of inductive and inductive-recursive definitions for that theory. He has also contributed to its categorical semantics (categories with families) and its proof theory (normalization by evaluation). Recently, he has outlined a new approach based on game semantics to Martin-Löf's fundamental meaning explanations for intuitionistic type theory.

Tuesday, November 24, 2015
2:00 PM
Gates & Hillman Centers 6501

Principles of Programming Seminars