@inproceedings{chapman2019system,
  title={System F in Agda, for fun and profit},
  author={Chapman, James and Kireev, Roman and Nester, Chad and Wadler, Philip},
  booktitle={International Conference on Mathematics of Program Construction},
  pages={255--297},
  year={2019},
  organization={Springer}
}