Types
Summarised papers
- Leveraging Rust types for modular specification and verification [astrauskas:oopsla:2019]
- Noninterference for free [bowman:icfp:2015]
- RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
- TALx86: A realistic typed assembly language [morrisett:wcsss:1999]
- Alias types [smith:esop:2000]
- A type system for expressive security policies [walker:popl:2000]
Unsummarised papers
- Unifying type checking and property checking for low-level code [condit:popl:2009]
- Secure information flow verification with mutable dependent types [ferraiuolo:dac:2017]
- Existential types for imperative languages [grossman:esop:2002]
- A polymorphic intermediate verification language: Design and logical encoding [leino:tacas:2010]
- Type-based decompilation (or program reconstruction via type reconstruction) [mycroft:esop:1999]
- Ynot: Dependent types for imperative programs [nanevski:icfp:2008]
- Specifying concurrent programs in separation logic: Morphisms and simulations [nanevski:oopsla:2019]
- Alias types for recursive data structures [walker:tic:2001]
- A dependently typed assembly language [xi:icfp:2001]
- Safe to the last instruction: automated verification of a type-safe operating system [yang:pldi:2010]