System F in Agda, for Fun and Profit

James Chapman; Roman Kireev; Chad Nester; Philip Wadler

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

System F in Agda, for Fun and Profit

James Chapman, Roman Kireev, Chad Nester, Philip Wadler

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

Abstract / Description of output

System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider Fωμ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script.

Original language	English
Title of host publication	Mathematics of Program Construction
Editors	Graham Hutton
Place of Publication	Cham
Publisher	Springer
Pages	255-297
Number of pages	43
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_10
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_10Licence: All Rights Reserved

System F in Agda_CHAPMAN_DOA14062019_AFVAccepted author manuscript, 219 KB

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

Cite this

@inproceedings{62107dbca5b74361a28d7ce0635f73c8,

title = "System F in Agda, for Fun and Profit",

abstract = "System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider Fωμ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script. ",

author = "James Chapman and Roman Kireev and Chad Nester and Philip Wadler",

year = "2019",

month = oct,

day = "20",

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

language = "English",

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

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

publisher = "Springer",

pages = "255--297",

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",

}

TY - GEN

T1 - System F in Agda, for Fun and Profit

AU - Chapman, James

AU - Kireev, Roman

AU - Nester, Chad

AU - Wadler, Philip

PY - 2019/10/20

Y1 - 2019/10/20

N2 - System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider Fωμ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script.

AB - System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider Fωμ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script.

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

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

M3 - Conference contribution

SN - 978-3-030-33635-6

T3 - Lecture Notes in Computer Science (LNCS)

SP - 255

EP - 297

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 -

System F in Agda, for Fun and Profit

Abstract / Description of output

Publication series

Conference

Access to Document

Fingerprint

Cite this