VaultA programming language of the C language family for security research. It includes a linear type system for managing resources: memory blocks, files, network connections, graphics contexts, and so forth. It also has a module system and support for first-class functions with lexical closure and the ability to curry or partially-apply functions.
Types are annotated with keys representing capabilities of some sort. Each computation's state includes a set of "held" keys, which provide access to resources.
- The project home page at Microsoft Research.