Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Programming Languages working group (PLX)
Programming Languages working group (PLX)

The Programing Languages working group investigates all aspects of programming language design and implementation. We aim to shape the future of software construction by developing new ways of programming. Our work spans a broad spectrum of research, ranging from the study of program semantics to via type systems, program logics and abstract interpretation to syntax and user interfaces.

Projects
  • Koka
    Koka is a function-oriented programming language that seperates pure values from side-effecting computations, where the effect of every function is automatically inferred. Koka has many features that help programmers to easily change their data types and code organization correctly, while having a small language core with a familiar JavaScript like syntax.
  • TouchDevelop
    Create apps everywhere on all your devices! For Windows Phone and the web. In the TouchDevelop programming environment you write scripts by tapping on the screen. You do not need a separate PC or keyboard. Scripts can perform various tasks similar to regular apps. Any TouchDevelop user can install, run, edit, publish scripts. You can share scripts with other people by publishing them to the TouchDevelop script bazaar, or by submitting them as an app to the Windows Store or Windows Phone Store.
  • The F* Project
    This web page describes a collection of projects all loosely connected to F*, a new higher-order, effectful programming language (like ML) designed with program verification in mind. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based. It also compiles securely to JavaScript, enabling safe interop with arbitrary, untrusted JavaScript libraries.
  • Concurrent Revisions
    The Revisions project introduces a novel programming model for concurrent, parallel, and distributed applications. It provides programmers with a simple, yet powerful and efficient mechanism (based on mutable snapshots and deterministic conflict resolution) to execute various application tasks in parallel even if those tasks access the same data and may exhibit read-write or write-write conflicts.
  • First-class Polymorphism
    Type inference systems for functional languages are usually based on Hindley-Milner, where polymorphism is restricted to let-bound values only. 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 annotations to still do predicatable inference.
  • Dafny: a language and program verifier for functional correctness
    Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs.
  • Boogie: An Intermediate Verification Language
    Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes Boogie programs as input.
  • VCC: A Verifier for Concurrent C
    VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity.
  • Code Contracts
    Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.
  • Spec#
    Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has been used to explore specifications and the dynamic/static tools that make use of them.
Publications