Game Semantics

Game Semantics

Here is a program I wrote to compute interaction traces between PCF terms, following the HO game semantics. Among other things, I used it to compute the picture displayed in the background. Please don't expect a clean and well commented source code; for the moment I don't have time to clean it up and make a proper release.

Any modern installation of Ocaml should compile it correctly. The (really minimal) makefile requires ocamlbuild. The current (quite hackish) display module requires the development version of strid. To use it (if compiled via ocamlbuild), run main.native, preferably through a wrapper such as ledit (i.e. run "ledit ./main.native"). First enter a PCF term, then type help for a list of possible commands.