Projects per year
Abstract
We study a class of quantitative models for higherorder computation: Lafont categories with (infinite) biproducts. Each of these has a complete “internal semiring” and can be enriched over its modules. We describe a semantics of nondeterministic PCF weighted over this semiring in which fixed points are obtained from the bifree algebra over its exponential structure. By characterizing them concretely as infinite sums of approximants indexed over nested finite multisets, we prove computational adequacy. We can construct examples of our semantics by weighting existing models such as categories of games over a complete semiring. This transition from qualitative to quantitative semantics is characterized as a “change of base” of enriched categories arising from a monoidal functor from coherence spaces to modules over a complete semiring. For example, the game semantics of Idealized Algol is coherence space enriched and thus gives rise to to a weighted model, which is fully abstract.
Original language  English 

Article number  104645 
Journal  Information and Computation 
Volume  275 
Early online date  12 Nov 2020 
DOIs  
Publication status  Published  31 Dec 2020 
Keywords
 Complete semirings
 Computational adequacy
 Fixed points
 Game semantics
 Linear logic
 Quantitative models
ASJC Scopus subject areas
 Theoretical Computer Science
 Information Systems
 Computer Science Applications
 Computational Theory and Mathematics
Fingerprint
Dive into the research topics of 'Weighted models for higherorder computation'. Together they form a unique fingerprint.Projects
 1 Finished

Semantic Types for Verified Program Behaviour
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council