Research group

Programming Languages and Tools Lab

How to keep a secret (or forget it) in Agda

April 11

Static information flow control (IFC) is a program analysis technique used to detect information leaks ("bad flows") in programs. I will give a brief overview of how IFC can be used in typed functional programming languages, such as OCaml or Haskell, and illustrate the connection between static IFC and so-called effect systems, which have traditionally been used to track computational side-effects such exceptions or I/O. To do so, I will show how a simple IFC system can directly be embedded in the purely functional language Agda.

The talk will involve life-coding in Agda, so I assume that the audience has some familiarity with basic functional programming concepts and ideally some experience with one of the aforementioned functional programming languages.

Speaker: Sandro Stucki (Postdoctoral researcher at Chalmers University of Technology)

Google Meet: