The Intellectual Ascent to Agda

This session applies denotative design, a methodology rooted in denotational semantics, to derive C++ programs from mathematical entities using Agda syntax. It focuses on designing simple, composable libraries with C++’s templating capabilities.