AARHUS, DENMARK
Department of Computer Science is hosting a summer school in Programming Languages, Logic and Software Security. The summer school will take place at INCUBA Katrinebjerg in Aarhus from August 10th -14th, 2026.
Speaker: Bas Spitters
Abstract:
The Rocq proof assistant aids us in constructing proofs in dependent type theory. In these lectures I will give an introduction to Rocq, its type theory, interactive theorem proving. Finally, I will highlight how proof assistant and GenAI form a unique marriage: GenAI speeds up proof search. Rocq makes sure that one can actually trust the proofs. These lectures form a practical counterpart to the introduction to type theory and a basis for program verification.
Speakers: Lars Birkedal and Amin Timany
Abstract:
Software bugs cost billions and can have severe consequences for the infrastructure we rely on. Formally proving program correctness is therefore of paramount importance. Hoare logic provides a framework for modular verification of programs. Separation logic extends Hoare logic with a powerful concept: separation—program modules working on disjoint resources can be reasoned about in isolation from one another.
Iris, the state-of-the-art Higher-Order Concurrent Separation Logic framework, extends this further by introducing reasoning principles such as higher-order impredicative invariants and user-defined ghost resources. These features are crucial for scaling the reasoning to highly concurrent programs with shared mutable state, featuring higher-order functions written in modern programming languages such as OCaml, Rust, and Go. This course is based on the Iris lecture notes and will enable students to specify and verify concurrent data structures and algorithms in Iris.
Speaker: Daniel Gratzer
Abstract:
Dependent type theory brings together ideas from logic and places them on top of a computational framework. The result is a complex (family of) systems which mix together ideas from mathematical logic, computer science, and (increasingly) category theory. In this course, we explore the foundations of dependent type theory with the aim of answering a few questions:
What ingredients make up a dependent type theory? How do we specify new dependent type theories? What properties do we wish to check hold for a particular type theory and why do we study them?
Along the way, we shall touch on why there are so many different flavors of type theory and how these systems relate to the proof assistants we'll use in other courses.
Speaker: Aslan Askarov
Abstract: TBD.
Speaker: Anders Møller
Abstract:
Static program analysis is the art of reasoning about the behavior of computer programs without actually running them. This is useful not only in optimizing compilers for producing efficient code but also for automatic error detection and other tools that can help programmers. Many software companies increasingly use static program analysis for preventing security vulnerabilities. This series of lectures will present essential principles and algorithms for static program analysis, based on material from cs.au.dk/~amoeller/spa/. The topics include basic dataflow analysis, interprocedural analysis, pointer analysis, control-flow analysis, and an introduction to the theory of abstract interpretation.
