How to keep a secret (or forget it) in Agda
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: https://meet.google.com/myu-dhmz-gvu