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.