Linearity and recursion in a typed Lambda-Calculus

Sandra Alves; Maribel Ferńandez; Ḿario Florido; Ian Mackie

doi:10.1145/2003476.2003500

Linearity and recursion in a typed Lambda-Calculus

Sandra Alves
, Maribel Ferńandez
, Ḿario Florido
, Ian Mackie

École Polytechnique

Ipatimup Diagnósticos
King's College London

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Citations (Scopus)

Abstract

We show that the full PCF language can be encoded in L_rec, a syntactically linear λ-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for L_rec, exploiting its linearity.

Original language	English
Title of host publication	PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
Pages	173-182
Number of pages	10
DOIs	https://doi.org/10.1145/2003476.2003500
Publication status	Published - 2 Sept 2011
Event	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark Duration: 20 Jul 2011 → 22 Jul 2011

Publication series

Name	PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

Conference

Conference	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
Country/Territory	Denmark
City	Odense
Period	20/07/11 → 22/07/11

Keywords

Linear λ-calculus
PCF
Recursion

Access to Document

10.1145/2003476.2003500

Cite this

Alves, S., Ferńandez, M., Florido, Ḿ., & Mackie, I. (2011). Linearity and recursion in a typed Lambda-Calculus. In PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming (pp. 173-182). (PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming). https://doi.org/10.1145/2003476.2003500

@inproceedings{6a2ec8386dab4edfac821160855791b2,

title = "Linearity and recursion in a typed Lambda-Calculus",

abstract = "We show that the full PCF language can be encoded in Lrec, a syntactically linear λ-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for Lrec, exploiting its linearity.",

keywords = "Linear λ-calculus, PCF, Recursion",

author = "Sandra Alves and Maribel Fer{\'n}andez and Ḿario Florido and Ian Mackie",

year = "2011",

month = sep,

day = "2",

doi = "10.1145/2003476.2003500",

language = "English",

isbn = "9781450307765",

series = "PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming",

pages = "173--182",

booktitle = "PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming",

note = "13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 ; Conference date: 20-07-2011 Through 22-07-2011",

}

Alves, S, Ferńandez, M, Florido, Ḿ & Mackie, I 2011, Linearity and recursion in a typed Lambda-Calculus. in PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming, pp. 173-182, 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011, Odense, Denmark, 20/07/11. https://doi.org/10.1145/2003476.2003500

Linearity and recursion in a typed Lambda-Calculus. / Alves, Sandra; Ferńandez, Maribel; Florido, Ḿario et al.
PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. 2011. p. 173-182 (PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Linearity and recursion in a typed Lambda-Calculus

AU - Alves, Sandra

AU - Ferńandez, Maribel

AU - Florido, Ḿario

AU - Mackie, Ian

PY - 2011/9/2

Y1 - 2011/9/2

N2 - We show that the full PCF language can be encoded in Lrec, a syntactically linear λ-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for Lrec, exploiting its linearity.

AB - We show that the full PCF language can be encoded in Lrec, a syntactically linear λ-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for Lrec, exploiting its linearity.

KW - Linear λ-calculus

KW - PCF

KW - Recursion

UR - https://www.scopus.com/pages/publications/80052153042

U2 - 10.1145/2003476.2003500

DO - 10.1145/2003476.2003500

M3 - Conference contribution

AN - SCOPUS:80052153042

SN - 9781450307765

T3 - PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

SP - 173

EP - 182

BT - PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

T2 - 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011

Y2 - 20 July 2011 through 22 July 2011

ER -

Linearity and recursion in a typed Lambda-Calculus

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this