Skip to main content

Agda−ventures with PolyP

Jeremy Gibbons and Patrik Jansson

Abstract

Revisiting Johan Jeuring's PolyP 30 years on, we note that a special-purpose language is no longer needed: general-purpose dependently typed programming suffices. This is a text-based adventure from software archeology, via codes to universes. Happy 60th Birthday, Johan!

Book Title
Taalblaat: Festschrift for Johan Jeuring
Editor
Alex Gerdes‚ Hieke Keuning‚ Wouter Swierstra
Year
2025