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.
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
- 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# 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.
- Sebastian Burckhardt, Principles of Eventual Consistency, vol. 1, no. 1-2, pp. 1-150, now publishers, 9 October 2014
- Daan Leijen, Koka: Programming with Row Polymorphic Effect Types, in Mathematically Structured Functional Programming 2014, EPTCS, 18 March 2014
- Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski, Replicated Data Types: Specification, Verification, Optimality, in 41st Symposium on Principles of Programming Languages (POPL), ACM SIGPLAN, 22 January 2014
- Sebastian Burckhardt, Manuel Fahndrich, Peli de Halleux, Jun Kato, Sean McDirmid, Michal Moskal, and Nikolai Tillmann, It's Alive! Continuous Feedback in UI Programming, in PLDI, ACM SIGPLAN, June 2013
- Sebastian Burckhardt, Alexey Gotsman, and Hongseok Yang, Understanding Eventual Consistency, no. MSR-TR-2013-39, March 2013
- Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Benjamin P. Wood, Cloud Types for Eventual Consistency, in Proceedings of the 26th European Conference on Object-Oriented Programming (ECOOP), Springer, 15 June 2012
- Cole Schlesinger and Nikhil Swamy, Verification Condition Generation with the Dijkstra State Monad, no. MSR-TR-2012-45, 22 April 2012
- Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv, Eventually Consistent Transactions, in Proceedings of the 22n European Symposium on Programming (ESOP), Springer, 24 March 2012
- Pierre-Yves Strub, Nikhil Swamy, Cedric Fournet, and Juan Chen, Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq, in In Proceedings of the ACM Symposium on Principles on Programming Languages, ACM, January 2012
- Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv, Eventually Consistent Transactions (full version), no. MSR-TR-2011-117, October 2011
- Daan Leijen, Sebastian Burckhardt, and Manuel Fahndrich, Prettier Concurrency: Purely Functional Concurrent Revisions, in Haskell Symposium 2011 (Haskell'11), ACM SIGPLAN, Tokyo, Japan, 7 July 2011
- Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks, Lightweight Monadic Programming in ML, in Proceedings of the International Conference of Functional Programming (ICFP'11), ACM SIGPLAN, Tokyo, Japan, 1 July 2011
- Mike Barnett, Manuel Fahndrich, K. Rustan M. Leino, Peter Mueller, Wolfram Schulte, and Herman Venter, Specification and Verification: The Spec# Experience, in Communications of the ACM, vol. 54, no. 6, pp. 81--91, Association for Computing Machinery, Inc., June 2011
- Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks, Lightweight Monadic Programming in ML, no. MSR-TR-2011-39, 24 March 2011
- Sebastian Burckhardt, Daan Leijen, and Manuel Fahndrich, Roll Forward, Not Back: A Case for Deterministic Conflict Resolution, in The 2nd Workshop on Determinism and Correctness in Parallel Programming (WODET'11), Newbeach, California, March 2011
- Mike Barnett and K. Rustan M. Leino, To Goto Where No Statement Has Gone Before, in VSTTE 2010, August 2010
- Mike Barnett, Manuel Fahndrich, and Francesco Logozzo, Embedded Contract Languages, in ACM SAC - OOPS, Association for Computing Machinery, Inc., March 2010
- Mike Barnett and K. Rustan M. Leino, Weakest-precondition of unstructured programs, in PASTE '05: The 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, ACM Press, New York, NY, USA, 2005