Unraveling Recursion: Compiling an IR with Recursion to System F

Michael Peyton Jones; Vasilis Gkoumas; Roman Kireev; Kenneth MacKenzie; Chad Nester; Philip Wadler

doi:10.1007/978-3-030-33636-3_15

Unraveling Recursion: Compiling an IR with Recursion to System F

Michael Peyton Jones, Vasilis Gkoumas, Roman Kireev, Kenneth MacKenzie, Chad Nester, Philip Wadler

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

Abstract / Description of output

Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higher-level features of programming languages. In this paper we show how toconstruct an IR based on System F_ω^μ which supports recursive functions and datatypes, and describe how to compile it to System F_ω^μ. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.

Original language	English
Title of host publication	Mathematics of Program Construction
Editors	Graham Hutton
Place of Publication	Cham
Publisher	Springer
Pages	414-443
Number of pages	30
ISBN (Electronic)	978-3-030-33636-3
ISBN (Print)	978-3-030-33635-6
DOIs	https://doi.org/10.1007/978-3-030-33636-3_15
Publication status	Published - 20 Oct 2019
Event	13th International Conference on Mathematics of Program Construction - Porto, Portugal Duration: 7 Oct 2019 → 9 Oct 2019 http://www.cs.nott.ac.uk/~pszgmh/mpc19.html

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Publisher	Springer, Cham
Volume	11825
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	13th International Conference on Mathematics of Program Construction
Abbreviated title	MPC 2019
Country/Territory	Portugal
City	Porto
Period	7/10/19 → 9/10/19
Internet address	http://www.cs.nott.ac.uk/~pszgmh/mpc19.html

Access to Document

10.1007/978-3-030-33636-3_15Licence: All Rights Reserved

Unravelling Recursion_JONES_DOA14062019_AFVAccepted author manuscript, 577 KB

https://link.springer.com/chapter/10.1007%2F978-3-030-33636-3_15Licence: All Rights Reserved

Cite this

@inproceedings{c609cc2cc28043d4bfd2b2bf720e44eb,

title = "Unraveling Recursion: Compiling an IR with Recursion to System F",

abstract = "Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higher-level features of programming languages. In this paper we show how toconstruct an IR based on System Fωμ which supports recursive functions and datatypes, and describe how to compile it to System Fωμ. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.",

author = "{Peyton Jones}, Michael and Vasilis Gkoumas and Roman Kireev and Kenneth MacKenzie and Chad Nester and Philip Wadler",

year = "2019",

month = oct,

day = "20",

doi = "10.1007/978-3-030-33636-3_15",

language = "English",

isbn = "978-3-030-33635-6",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "414--443",

editor = "Graham Hutton",

booktitle = "Mathematics of Program Construction",

note = "13th International Conference on Mathematics of Program Construction, MPC 2019 ; Conference date: 07-10-2019 Through 09-10-2019",

url = "http://www.cs.nott.ac.uk/~pszgmh/mpc19.html",

}

Peyton Jones, M, Gkoumas, V, Kireev, R, MacKenzie, K, Nester, C & Wadler, P 2019, Unraveling Recursion: Compiling an IR with Recursion to System F. in G Hutton (ed.), Mathematics of Program Construction. Lecture Notes in Computer Science (LNCS), vol. 11825, Springer, Cham, pp. 414-443, 13th International Conference on Mathematics of Program Construction, Porto, Portugal, 7/10/19. https://doi.org/10.1007/978-3-030-33636-3_15

TY - GEN

T1 - Unraveling Recursion: Compiling an IR with Recursion to System F

AU - Peyton Jones, Michael

AU - Gkoumas, Vasilis

AU - Kireev, Roman

AU - MacKenzie, Kenneth

AU - Nester, Chad

AU - Wadler, Philip

PY - 2019/10/20

Y1 - 2019/10/20

N2 - Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higher-level features of programming languages. In this paper we show how toconstruct an IR based on System Fωμ which supports recursive functions and datatypes, and describe how to compile it to System Fωμ. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.

AB - Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higher-level features of programming languages. In this paper we show how toconstruct an IR based on System Fωμ which supports recursive functions and datatypes, and describe how to compile it to System Fωμ. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.

U2 - 10.1007/978-3-030-33636-3_15

DO - 10.1007/978-3-030-33636-3_15

M3 - Conference contribution

SN - 978-3-030-33635-6

T3 - Lecture Notes in Computer Science (LNCS)

SP - 414

EP - 443

BT - Mathematics of Program Construction

A2 - Hutton, Graham

PB - Springer

CY - Cham

T2 - 13th International Conference on Mathematics of Program Construction

Y2 - 7 October 2019 through 9 October 2019

ER -

Unraveling Recursion: Compiling an IR with Recursion to System F

Abstract / Description of output

Publication series

Conference

Access to Document

Fingerprint

Cite this