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