RSS Meetups are monthly gatherings of LASIGE members with interests in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, Formal methods and other topics.

Title: Dependent types for parallel programming

Presenter: Vasco T. Vasconcelos

We present a type discipline for parallel programs. The model we have in mind comprises a fixed number of processes running in parallel and communicating via collective operations or point-to-point synchronous message exchanges. A type describes the protocol to be followed by all processes in a given program. We present the type theory, a core imperative programming language and its operational semantics, and prove that type checking is decidable and that well-typed programs do not deadlock. The talk is accompanied by a large number of examples drawn from the literature on parallel programming.

[Joint work with Francisco Martins, Nobuko Yoshida, and Hugo A. López]