David Sankel: The Intellectual Ascent to Agda

David Sankel explains how to apply denotational semantics and denotative design to derive robust C++ programs using the Agda language.

When one thinks of math and computer science what often comes to mind are asymptotic analysis and mind-bending algorithms for physical simulations. A branch that usually slips through cracks is denotational semantics, the math of syntax and meaning. Denotative design, denotational semantics put into practice, is a top-down design methodology that produces simple, composable, and incredibly powerful libraries that are in an entirely different league from what is commonly available. It is especially suited to C++ which has a sufficiently powerful templating engine. In this session, we will learn how to apply denotative design by deriving C++ programs from domain-specific mathematical entities using the syntax of Agda, a pure functional and dependently-typed language. --- *--* ---