Language-Based Security — AU PLS Summer School 2026

Material from my mini course on language-based security at the PLS Summer School, Aarhus, 10–14 August 2026. Comments, questions and corrections are welcome — please email aslan@cs.au.dk.

Day 1 (Aug 10). How to read a PL security paper

{Slides}

Extra material:

• Video recording of an earlier version of this talk, given at PLMW@PLDI 2024.

Day 2 (Aug 11). Introduction to information flow and knowledge-based IFC specification

{Slides for Day 2 and 3}

Index cards (PINI and PSNI are progress-insensitive and progress-sensitive noninterference).

Reading:

• Sections 1 and 2 of Attacker Control and Impact for Confidentiality and Integrity by A. Askarov and A. Myers, Logical Methods in Computer Science, 2011.

Day 3 (Aug 13). Type-based enforcement

Reading:

• Termination-Insensitive Noninterference Leaks More Than Just a Bit by A. Askarov, S. Hunt, A. Sabelfeld and D. Sands, ESORICS 2008.
• Reconciling progress-insensitive noninterference and declassification by J. Bay and A. Askarov, CSF 2020 (IEEE).

Extra material:

• SmallStepNI: a Rocq mechanization of the noninterference proof for the Volpano–Smith–Irvine type system. The notes differ in the security condition, targeting the termination-insensitive noninterference theorem instead of PINI, but the mechanics of the proof are identical.
• infoflow-basics.pdf: notes on the proof technique and its background.

Day 4 (Aug 14). The downgrading semantics of memory safety

{Slides}

PLDI 2026 paper and related artifacts:

• R. R. Hansen, A. S. Larsen and A. Askarov. The Downgrading Semantics of Memory Safety. Proc. ACM Program. Lang. 10, PLDI, Article 182, June 2026. doi:10.1145/3808260 · ACM DL · arXiv
• Artifact (Zenodo)
• Notac — in-browser demo of the Notac language, its semantics, and examples.

Background reading:

• The Meaning of Memory Safety by A. Azevedo de Amorim, C. Hriţcu and B. C. Pierce, POST 2018.

Extra material:

• Video recording of the PLDI 2026 presentation, given by R. R. Hansen.

Last updated 15 August 2026.