## 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 | |

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 |

## Fingerprint

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