Abstract:

Verification of concurrent software is a notoriously difficult

subject, whose complexities stem from the inability of the

existing verification methods to modularize, and thus divide and

conquer the verification problem.

Dependent types are a formal method well-known for its ability to

modularize and scale complex mathematical proofs. But, when it

comes to programming, dependent types are considered limited to

the purely functional programming model.

In this talk I will present my recent work towards reconciling

dependent types with shared memory concurrency, with the goal of

achieving modular verification for the latter. Applying the

type-theoretic paradigm to concurrency have lead to interesting

reformulations of some classical verification ideas, and to the

discovery of novel and useful abstractions for modularizing the

proofs.