POPL-Related Microsoft Research Technologies

Principles of Programming Languages 2013
January 23–25, 2013 | Rome, Italy

Learn about Microsoft Research programming language, development, and verification tools that you can download or use via the web.

Programming Languages, Development, and Education

Code Contracts 

Code Contracts provide a language-agnostic way to express coding assumptions in Microsoft .NET programs. Code Contracts tools include a runtime checker, a static checker based on abstract interpretation, and a documentation generator. 

  • See VMCAI paper, “Automatic Inference of Necessary Preconditions.”  
F# 3.0 

F# 3.0 extends the succinct and expressive F# language so that you can program directly against rich spaces of data and services, such as databases, web services, web data feeds, and data brokers. F# is an open-source, cross-platform language and has an active community led by the F# Software Foundation. The Visual F# tools are developed by the Microsoft Developer Division. 

Try F# 

Try F# lets you program F# 3.0 in your web browser to explore its unique new features for information-rich programming. The site contains tutorials for learning F#, as well as applied topics such as data science, financial computing, statistics, numerical computing, visualization, and machine learning. You can create, open, and share your files directly from the site—including embedding code in your own blog, website, or posting on Twitter and Facebook.

  • See POPL paper, "Abstraction and Invariance for Algebraically Indexed Types." The paper explores the semantics of types related to F#'s units of measure.

GHCGHC is the world’s leading Haskell compiler. It offers a particularly rich type system (for example, type classes, GADTs, kind polymorphism, type families and associated types, and deferred type errors). It is extensible through its support for meta-programming, user-written rewrite rules and plug-ins, and the entire compiler is available as a library. It runs out of the box on multicore processors, supporting many different parallelism paradigms including transactional memory, semi-implicit parallelism, and data parallelism. 

  • See POPL paper, “HALO: from Haskell to First-Order Logic through Denotational Semantics.”

Infer.NET FunInfer.NET Fun turns the simple succinct syntax of F# into an executable modelling language for Bayesian machine learning. We propose a marriage of probabilistic functional programming with Bayesian reasoning. Infer.NET Fun turns F# into a probabilistic modelling language—you can code the conditional probability distributions of Bayes’ rule by using F# array comprehensions with constraints. Write your model in F#. Run it directly to synthesize test datasets and to debug models. Or compile it with Infer.NET for efficient statistical inference. Hence, efficient algorithms for a range of regression, classification, and specialist learning tasks derive by probabilistic functional programming.


  • See POPL paper, “A Model-Learner Pattern for Bayesian Reasoning.”
  • See Andy Gordon's keynote at OBT on “Probabilistic Programming.”
Pex for fun 

Pex for fun brings programming in C#, Microsoft Visual Basic, and F# to your web browser. Click the Ask Pex! button to compile, run, and analyze your code by using the automatic test generation capabilities of Pex. Interactive code duels challenge you to write code that matches a secret implementation. Many teachers are using Pex for fun in their courses today.  


TouchDevelop  TouchDevelop is a radically new browser-based software development environment, bringing the excitement of the first programmable personal computers to tablets. Program with the TouchDevelop Web App from your iPad, Android tablet, or Windows 8 device. 

Verification Tools

BEK is a domain-specific language for writing common string manipulating functions and is combined with state-of-the-art analysis based on symbolic transducers (see POPL paper by Veanes et al.) With BEK, you can answer questions like: “Are these two programs equivalent?” or “Does the order matter?”

  • See VMCAI paper, “Static Analysis of String Encoders and Decoders.”

Dafny is an imperative, object-oriented programming language with classes and inductive datatypes, and specification constructs for describing intended behavior. The Dafny static verifier, built on Boogie, checks the consistency of the program and these specifications.


F* is a new verification-oriented language based on F#. Specifications in F* are stated by using dependent types, and its certified typechecker makes use of an SMT solver to provide a powerful, semi-automated way to certify the correctness of higher-order programs. F* compiles to Microsoft .NET bytecode in a type-preserving style.  

  • See POPL paper, “Fully Abstract Compilation to JavaScript.”

PoirotPoirot is a static analysis tool for helping programmers detect and debug errors in concurrent and asynchronous systems. Poirot can detect application-specific errors, including data races, deadlocks, assertion failures, and protocol violations.


Seal is a research prototype that can infer the potential side effects of methods in a C# program. The side effects of a method are the set of heap locations in the program state right before the invocation of the method (referred to as prestate) that are modified (or written) by the method. Seal supports many sophisticated (and higher-order) C# features, such as LINQ, delegates, event-handler, and exceptions.

SLAyer is a program analysis tool that is designed to prove the absence of memory safety errors by using separation logic. SLAyer is aimed at moderately sized (10–30K) systems-level code bases written in C; it is fully automatic and does not require annotations or hints from the programmer.

The TLA Toolbox is an IDE for writing and running debugging tools on specifications written in the TLA+ language, a very expressive high level specification language. Writing and checking TLA+ specs enables software designers to catch errors before any code is written, complementing the many tools for finding coding errors.

VCCVCC is an industrial-strength verification environment (deductive verifier, verification debugger, proof progress monitor, and IDE integration) for low-level concurrent systems code written in C. VCC has been used to verify the functional correctness of tens of thousands of lines of commercial operating system code.

Verification Infrastructure

Boogie is a first-order intermediate verification language, used by program verifiers, program checkers, and other program analyzers to formulate verification conditions (VCs). More than a dozen verification tools are built on Boogie, including VCC, HAVOC, Dafny, and Chalice. Boogie uses Z3 to discharge VCs.

Symbolic Automata is a toolkit that lifts classical automata analysis to work modulo rich alphabet theories. The toolkit supports analysis of finite symbolic automata and symbolic transducers, internalizing automata as Z3 theories.

  • See VMCAI paper, “Static Analysis of String Encoders and Decoders.”

Z3 is a high-performance theorem prover that supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. 

  • Now available: Z3 source code.
  • See OBT paper, "Fast Analysis of Biological Models Using Open-World Logic Programming."
Top of page


Event Website
Related Microsoft Groups and Labs