Agda by Example: Programming and Proving with Dependent Types

Agda by Example: Programming and Proving with Dependent Types is a hands-on introduction to one of the most elegant verification tools in modern functional programming. Participants will learn how to write total programs, encode invariants directly in types, and develop machine-checked proofs alongside executable code. Through live examples and small guided exercises, we’ll build data structures, manipulate dependently typed vectors, prove algebraic properties, and construct verified functions that cannot go wrong. This tutorial is designed for software engineers and functional programmers who are curious about rigorous correctness, type-driven development, and the practical side of theorem proving. No prior experience with proof assistants is required—only familiarity with functional programming concepts. Come discover how Agda turns specifications into code, and code into proofs, all by example.

Peter Thiemann

Peter Thiemann is a professor at the university of Freiburg and leads the programming languages group at the institute of computer science. His research interests are focused on programming with types, in particular functional programming and concurrent programming.