RSS Meetup (October 2018)
Part of Relation 913
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]