Mr Thomas Cuvillier
Postdoctoral Research Assistant
Research Interests:The context of my work is the game semantics of programs. This is part of the more general denotational semantics field, that strives to devise proper mathematical models for software. The purpose of semantics is to both define the meaning of the programs and serve as basis for analysis and verification. The games have proven to be extremely powerful to provide a fully abstract denotational semantics for different theoretical programming languages. However, until recently, games were dealing with names and variables using so-called ``bad variables", that were preventing them from being a complete model for resource generation. In order to solve this problem, nominal games were introduced. These games now live in an non-standard model of set-theory named nominal set-theory. This allows the type of the variable to be the one of the object it stores, and provides clean treatment of names and their creation.
My work now focus on building the first ever fully complete model of a well-spread, highly powerful and hugely used programming language, ML.