System F in Agda, for Fun and Profit

James Chapman, Roman Kireev, Chad Nester, Philip Wadler

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationMathematics of Program Construction
EditorsGraham Hutton
Place of PublicationCham
PublisherSpringer International Publishing
Number of pages43
ISBN (Electronic)978-3-030-33636-3
ISBN (Print)978-3-030-33635-6
Publication statusPublished - 20 Oct 2019
Event13th International Conference on Mathematics of Program Construction - Porto, Portugal
Duration: 7 Oct 20199 Oct 2019

Publication series

Name Lecture Notes in Computer Science (LNCS)
PublisherSpringer, Cham
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Conference on Mathematics of Program Construction
Abbreviated titleMPC 2019
Internet address


Dive into the research topics of 'System F in Agda, for Fun and Profit'. Together they form a unique fingerprint.

Cite this