Weighted relational models of typed Lambda-Calculi

J D Laird, Giulio Manzonetto, Guy Mccusker, Michele Pagani

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 16 Citations

Abstract

The category Rel of sets and relations yields one of the simplest denotational semantics of Linear Logic (LL). It is known that Rel is the biproduct completion of the Boolean ring. We consider the generalization of this construction to an arbitrary continuous semiring R, producing a cpo-enriched category which is a semantics of LL, and its (co)Kleisli category is an adequate model of an extension of PCF, parametrized by R. Specific instances of R allow us to compare programs not only with respect to "what they can do", but also "in how many steps" or "in how many different ways" (for non-deterministic PCF) or even "with what probability" (for probabilistic PCF).
LanguageEnglish
Title of host publication2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)
Place of PublicationLos Alamitos, California
PublisherIEEE
Pages301-310
Number of pages10
ISBN (Print)9781479904136
DOIs
StatusPublished - 1 Jun 2013
Event2013 Twenty-Eighth Annual IEEE/ACM Symposium on Logic in Computer Science (LICS 2013) - New Orleans, LA, USA, UK United Kingdom
Duration: 25 Jun 201328 Jun 2013

Publication series

NameAnnual IEEE/ACM Symposium on Logic in Computer Science (LICS)
ISSN (Print)1043-6871

Conference

Conference2013 Twenty-Eighth Annual IEEE/ACM Symposium on Logic in Computer Science (LICS 2013)
CountryUK United Kingdom
CityNew Orleans, LA, USA
Period25/06/1328/06/13

Fingerprint

Typed lambda Calculus
Relational Model
Linear Logic
Boolean Ring
Enriched Category
Denotational Semantics
Semiring
Completion
Arbitrary
Model
Generalization
Semantics

Cite this

Laird, J. D., Manzonetto, G., Mccusker, G., & Pagani, M. (2013). Weighted relational models of typed Lambda-Calculi. In 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS) (pp. 301-310). (Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)). Los Alamitos, California: IEEE. DOI: 10.1109/LICS.2013.36

Weighted relational models of typed Lambda-Calculi. / Laird, J D; Manzonetto, Giulio; Mccusker, Guy; Pagani, Michele.

2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS). Los Alamitos, California : IEEE, 2013. p. 301-310 (Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Laird, JD, Manzonetto, G, Mccusker, G & Pagani, M 2013, Weighted relational models of typed Lambda-Calculi. in 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS). Annual IEEE/ACM Symposium on Logic in Computer Science (LICS), IEEE, Los Alamitos, California, pp. 301-310, 2013 Twenty-Eighth Annual IEEE/ACM Symposium on Logic in Computer Science (LICS 2013), New Orleans, LA, USA, UK United Kingdom, 25/06/13. DOI: 10.1109/LICS.2013.36
Laird JD, Manzonetto G, Mccusker G, Pagani M. Weighted relational models of typed Lambda-Calculi. In 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS). Los Alamitos, California: IEEE. 2013. p. 301-310. (Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)). Available from, DOI: 10.1109/LICS.2013.36
Laird, J D ; Manzonetto, Giulio ; Mccusker, Guy ; Pagani, Michele. / Weighted relational models of typed Lambda-Calculi. 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS). Los Alamitos, California : IEEE, 2013. pp. 301-310 (Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)).
@inproceedings{919dcd87f7894c228578c899ead68476,
title = "Weighted relational models of typed Lambda-Calculi",
abstract = "The category Rel of sets and relations yields one of the simplest denotational semantics of Linear Logic (LL). It is known that Rel is the biproduct completion of the Boolean ring. We consider the generalization of this construction to an arbitrary continuous semiring R, producing a cpo-enriched category which is a semantics of LL, and its (co)Kleisli category is an adequate model of an extension of PCF, parametrized by R. Specific instances of R allow us to compare programs not only with respect to {"}what they can do{"}, but also {"}in how many steps{"} or {"}in how many different ways{"} (for non-deterministic PCF) or even {"}with what probability{"} (for probabilistic PCF).",
author = "Laird, {J D} and Giulio Manzonetto and Guy Mccusker and Michele Pagani",
year = "2013",
month = "6",
day = "1",
doi = "10.1109/LICS.2013.36",
language = "English",
isbn = "9781479904136",
series = "Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)",
publisher = "IEEE",
pages = "301--310",
booktitle = "2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)",
address = "USA United States",

}

TY - GEN

T1 - Weighted relational models of typed Lambda-Calculi

AU - Laird,J D

AU - Manzonetto,Giulio

AU - Mccusker,Guy

AU - Pagani,Michele

PY - 2013/6/1

Y1 - 2013/6/1

N2 - The category Rel of sets and relations yields one of the simplest denotational semantics of Linear Logic (LL). It is known that Rel is the biproduct completion of the Boolean ring. We consider the generalization of this construction to an arbitrary continuous semiring R, producing a cpo-enriched category which is a semantics of LL, and its (co)Kleisli category is an adequate model of an extension of PCF, parametrized by R. Specific instances of R allow us to compare programs not only with respect to "what they can do", but also "in how many steps" or "in how many different ways" (for non-deterministic PCF) or even "with what probability" (for probabilistic PCF).

AB - The category Rel of sets and relations yields one of the simplest denotational semantics of Linear Logic (LL). It is known that Rel is the biproduct completion of the Boolean ring. We consider the generalization of this construction to an arbitrary continuous semiring R, producing a cpo-enriched category which is a semantics of LL, and its (co)Kleisli category is an adequate model of an extension of PCF, parametrized by R. Specific instances of R allow us to compare programs not only with respect to "what they can do", but also "in how many steps" or "in how many different ways" (for non-deterministic PCF) or even "with what probability" (for probabilistic PCF).

UR - http://dx.doi.org/10.1109/LICS.2013.36

U2 - 10.1109/LICS.2013.36

DO - 10.1109/LICS.2013.36

M3 - Conference contribution

SN - 9781479904136

T3 - Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)

SP - 301

EP - 310

BT - 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)

PB - IEEE

CY - Los Alamitos, California

ER -