Quantitative semantics of the lambda calculus: Some generalisations of the relational model

Conference item

We present an overview of some recent work on the quantitative semantics of the 𝛌-calculus. Our starting point is the fundamental degenerate model of linear logic, the relational model. We show that three quantitative semantics of the simplytyped 𝛌-calculus are equivalent: the relational semantics, HO/N game semantics, and the Taylor expansion semantics. We then consider two recent generalisations of the relational model: first, R-weighted relational models where R is a complete commutative semiring, as studied by Laird et al.; secondly, generalised species of structures, as introduced by Fiore et al. In each case, we briefly discuss some applications to quantitative analysis of higher-order programs.

Authors: Ong, C

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Institute of Electrical and Electronics Engineers
• Host title: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
• Journal: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
• Publication date: 2017-08-01
• Acceptance date: 2017-05-12
• DOI: 10.1109/LICS.2017.8005064
• ISBN: 9781509030187