Code Contracts for .NET  

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of pre-conditions, post-conditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking (via code rewriting), enable static contract verification (e.g. via abstract interpretation), and documentation generation.

Home

Task Parallel Library, strutured concurrency

The Task Parallel Library is designed to make it much easier to write managed code that can automatically use multiple processors. Using the library, you can conveniently express potential parallelism in existing sequential code, where the exposed parallel tasks will be run concurrently on all available processors. The TPL can be seen as a domain specific embedded language for expressing concurrency through the use of first-class anonymous functions (delegates) and parametric polymorphism (generics). Currently, the TPL library is part of the Parallel extensions to .NET that ships as part of .NET 4.0.

Home MSDN article Channel 9 Video  

Typed Assembly Languages 

We study techniques to guarantee safety properties of native code through typed intermediate languages and Typed Assembly Languages (TAL). TAL requires that the compiler generate native code with type annotations and a verifier check the annotated native code. This way, we do not have to trust the compiler. We focus on large-scale optimizing object-oriented compilers.

Home  

First-class Polymorphism

Type inference systems for functional languages are usually based on Hindley-Milner. Unfortunately, polymorphism in Hindley-Milner is restricted to let-bound values only which restricts expressiveness. An long standing research challenge is to do type inference for full System-F where polymorphism is first-class and where polymorphic values can be passed as arguments or be part of data structures. Since type inference for System-F is undecidable in general, the question is how to use the minimal amount of type annotations to make type inference decidable. We designed two systems HMF and HML that both reside at interesting corners of the design space.

Home  

Singularity, operating system prototype

Singularity is a research project focused on the construction of dependable systems through innovation in the areas of systems, languages, and tools. We are building a research operating system prototype (called Singularity), extending programming languages, and developing new techniques and tools for specifying and verifying program behavior.

Home | Downloads | Publications