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 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. 
 

• See DDFP 2013.

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.

GHC 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 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 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.  

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."