(PolyP at 30)

This repository contains the literate Agda file which doubles as the LaTeX source for the paper and the Agda code in it.

The Agda code typechecks at least with version 2.7.0.1 of Agda and version 2.2 of the Agda standard library.

The paper is a chapter in a Festschrift for Johan Jeuring’s 60:th birthday celebration: JohanFest, Utrecht, 2025-09-19.

At JohanFest, Patrik Jansson presented some slides based on the paper and recollections from our joint work over the decades.

@inproceedings{GibbonsJansson2025_agda-ventures,
  title = "Agda-ventures with PolyP",
  author = "Jeremy Gibbons and Patrik Jansson",
  year = 2025,
  pages = {21--36},
  booktitle = "Taalblaat: Festschrift for Johan Jeuring",
  editor = "Alex Gerdes and Hieke Keuning and Wouter Swierstra",
  url = "https://github.com/DSLsofMath/PolyP30/raw/main/GibbonsJansson_PolyP30.pdf",
  doi = "10.5281/zenodo.17181794"
}