System F in Agda, for fun and profit

DOI10.1007/978-3-030-33636-3_10zbMath1434.68079OpenAlexW2980703959MaRDI QIDQ2176683

Roman Kireev, Chad Nester, Philip Wadler, James T. E. Chapman

Publication date: 5 May 2020

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/129967822/System_F_in_Agda_CHAPMAN_DOA14062019_AFV.pdf

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Extracting functional programs from Coq, in Coq

Uses Software

• Coq
• Twelf
• Agda
• PoplMark

This page was built for publication: System F in Agda, for fun and profit