Projects per year
Abstract
We describe an interpretation of recursive computation in a symmetric monoidal category with infinite biproducts and cofree commutative comonoids (for instance, the category of free modules over a complete semiring). Such categories play a significant role in ``quantitative'' models of computation: they bear a canonical complete monoid enrichment, but may not be cpoenriched, making standard techniques for reasoning about fixed points unavailable. By constructing a bifree algebra for the cofree exponential, we obtain fixed points for morphisms in its coKleisli category without requiring any ordertheoretic structure. These fixed points corresponding to infinite sums of finitary approximants indexed over the nested finite multisets, each representing a unique callpattern for computation of the fixed point. We illustrate this construction by using it to give a denotational semantics for PCF with nondeterministic choice and scalar weights from a complete semiring, proving that this is computationally adequate with respect to an operational semantics which evaluates a term by taking a weighted sum of the residues of its terminating reduction paths.
Original language  English 

Title of host publication  LICS '16, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science 
Editors  Natarajan Shankar 
Place of Publication  New York, U. S. A. 
Publisher  Association for Computing Machinery 
Pages  347356 
Number of pages  10 
ISBN (Print)  9781450343916 
DOIs  
Publication status  Published  5 Jul 2016 
Event  31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016  New York, USA United States Duration: 5 Jul 2016 → 8 Jul 2016 
Publication series
Name  Proceedings  Symposium on Logic in Computer Science 

Publisher  IEEE 
ISSN (Electronic)  25755528 
Conference
Conference  31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 

Country  USA United States 
City  New York 
Period  5/07/16 → 8/07/16 
Fingerprint Dive into the research topics of 'Fixed points in quantitative semantics'. 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