Variations in F#

As a functional programming language, F# makes it easy to express complex ideas in a succinct way. F# is also a statically typed and compiled, which means that it can be used to build efficient implementations. This makes it a great language for implementing research projects and prototypes.

Additionaly, F# is distributed with a source code under a license that allows modification for academic purposes. This opens the possibility for programming language research based on the F# language. A modified version of F# built from the source code can be easily integrated in MonoDevelop using the open-source language binding.

The rest of the page lists several interesting research projects that either extend F# or were created mainly using F#. Below you can also find a list of recent publications related to the F# language itself. If you know about (or work on) a project that uses F# and is not in the list, please let us know.

Related Research Projects

F7: Refinement Types for F#

Karthik Bhargavan, C??dric Fournet and Andy Gordon, Microsoft Research Cambridge

F7 is an enhanced typechecker for F#. F7 supports static checking of properties expressed with refinement types. The motivation is to check various security properties of F# implementation code by typing. For more information about the project, visit the project homepage.


A collaboration between EMIC, Aachen, Germany and the RiSE group, MSR Redmond

VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifi­cations. VCC is implemented in F#.

Academic Publications about F#

Joinads: a retargetable control-flow construct for reactive, parallel and concurrent programming

Tomas Petricek and Don Syme

Modern challenges led to a design of a wide range of programming models for reactive, parallel and concurrent programming, but these are often difficult to encode in general purpose languages. We present an abstract type of computations called joinads together with a syntactic language extension that aims to make it easier to use joinads in modern functional languages.

Our extension generalizes pattern matching to work on abstract computations. It keeps a familiar syntax and semantics of pattern matching making it easy to reason about code, even in a non-standard programming model. We demonstrate our extension using three important programming models ??? a reactive model based on events; a concurrent model based on join calculus and a parallel model using futures. All three models are implemented as libraries that benefit from our syntactic extension. This makes them easier to use and also opens space for exploring new useful programming models.

The F# Asynchronous Programming Model

Don Syme, Tomas Petricek and Dmitry Lomov

We describe the asynchronous programming model in F#, and its applications to reactive, parallel and concurrent programming. The key feature combines a core language with a non-blocking modality to author lightweight asynchronous tasks, where the modality has control flow constructs that are syntactically a superset of the core language and are given an asynchronous semantic interpretation. This allows smooth transitions between synchronous and asynchronous code and eliminates callback-style treatments of inversion of control, without disturbing the foundation of CPU-intensive programming that allows F# to interoperate smoothly and compile efficiently to .NET and native code. An adapted version of the idea presented in this paper is under consideration for addition to the C# programming language.

Collecting Hollywood???s Garbage: Avoiding Space-Leaks in Composite Events

Tomas Petricek and Don Syme

The reactive programming model is largely different to what we???re used to as we don???t have full control over the application???s con-trol flow. If we mix the declarative and imperative programming style, which is usual in the ML family of languages, the situation is even more complex. It becomes easy to introduce patterns where the usual garbage collector for objects cannot automatically dispose all components that we intuitively consider garbage.

In this paper we discuss a duality between the definitions of garbage for objects and events. We combine them into a single one, to specify the notion of garbage for reactive programming model in a mixed functional/imperative language and we present a formal algorithm for collecting garbage in this environment.

Building on top of the theoretical model, we implement a library for reactive programming that does not cause leaks when used in the mixed declarative/imperative model. The library allows us to safely combine both of the reactive programming patterns. As a result, we can take advantage of the clarity and simplicity of the declarative approach as well as the expressivity of the imperative model.