Carnegie Mellon University in Qatar
School of Computer Science, Carnegie Mellon University
Supported by the Qatar National Research Fund


Formal Reasoning about Languages for Distributed Computation

Project Description

Foundational research in programming language semantics has given us the ability to design languages for sequential programming with strong theoretical properties, which translate into run-time assurance for programs written in such languages. Recently, logical frameworks such as Twelf and Coq have been used to formally prove deep properties of full-scale practical programming languages, such as the safety of Standard ML or the correctness of a compiler for an expressive subset of C. In contrast, no overarching methodologies exist yet for languages for distributed computation, which are gaining prominence with the advent of web programming, security infrastructures, and cloud computing. This means that we cannot say as much about the properties of present languages in these domains as a whole, or behaviors of specific programs written in them.
This project aims at developing recent work on language specification with substructural operational semantics (SSOS) into methodologies for designing and reasoning about programming and specification languages for distributed computation. We use the Concurrent Logical Framework (CLF) in order to elegantly implement SSOS specifications, and to develop and implement (co)inductive techniques to reason about such specification. Finally, we carry out case studies with logically-based languages for distributed computation such as ML5 to demonstrate the practicality of our approach.
This work was funded by the Qatar National Research Fund as project NPRP 09-1107-1-168 (Formal Reasoning about Languages for Distributed Computation) for an amount of $1,002,161 over 3 years.



Past members


2013 2012 2011
2013 2012

Related Work