Teaching Types and Non-Interference in Dafny
summary
Covers a Dafny-based teaching unit that connects programming-language concepts to concrete Dafny encodings and uses scaffolded assignments for Masters students. Explains proving type safety and non-interference (for a security type system and for a dynamic taint tracker) in a simplified C-like language, and reports lessons learned from four course offerings.
AI-written summary · about