Exploratory action

CANofGAS

Cost ANalyses of GAme Semantics
Cost ANalyses of GAme Semantics

Two independent success stories in the study of higher-order programming languages, which are subtle languages where the inputs and the outputs of a program are not simply numbers, strings, or compound data types but can themselves be programs, are:

1) the reshaping of the semantics description of programs as games (rather than functions), and

2) the recent development of reasonable complexity measures, allowing for meaningful cost analyses (which were not previously available).

CANofGAS aims at joining these two research directions, developing cost models for the games semantics of higher-order programs. In particular, we aim at modeling the efficient call-by-need evaluation scheme, at work for instance in the Haskell language and in the Coq proof assistant, and which admits a theory of costs but not yet a games semantics.

Inria teams involved
GALLINETTE, PARTOUT

Contacts

Beniamino Accattoli

Scientific leader

Guilhem Jaber

Scientific co-leader