Quantitative relational models of lambda-calculi

Photograph of Guy McCusker

Guy McCusker

(University of Bath)

The category of sets and relations, and its refinements, provides a setting for simple models of the lambda-calculus, including Scott's graph model and Girard's coherence spaces model. In such models, the denotation of a lambda term is a relation whose entries record qualitative facts about the behaviour of the term: "what it can do."

We investigate how to augment such models with quantitative information, so that the model can tell us not only what a term can do, but (for instance) "in how many ways" (for nondeterministic calculi), "with what probability" (for probabilistic calculi), or "in how many steps of computation". We present a general construction of quantitative relational models and a generic soundness theorem for them, and indicate the links with known quantitative models such as probabilistic coherence spaces.

This is joint work with Jim Laird (Bath), Giulio Manzonetto (Paris 13) and Michele Pagani (Paris 13))
Thursday 8th November 2012, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science