Peter Dybjer
Professor of Computer Science-Chalmers University of Technology, Gothenburg, Sweden
Game Semantics and Normalization by Evaluation
Abstract:
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).
Bio: 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.