Design of programming language features, type systems, program analysis and runtime systems.
|
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. |
|
|
Spec# is a programming system aimed at improving the development and maintenance of correct software. It consists of the Spec# programming language (a superset of the object-oriented .NET language C#, adding non-null types and code contracts), the Spec# compiler (which emits run-time checks to enforce the contracts), and the Boogie-based static program verifier (which attempts to prove a program correct with respect to its contracts). |
|
|
We seek to tolerate and correct memory errors including buffer overruns and dangling pointer errors by providing probabilistic memory safety. Using combinations of randomization, replication, and over-provisioning, we are able to provide the illusion that every object exists in its own infinite sub-heap. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
Executable specification language based on the theory of Abstract State Machines. |
|
|
C-Omega is a research project that explores language extensions in a couple domains. One is database integration, the other is XML. |
|
