[PL-sem-jr] Talk tomorrow, Thu 1/20

[Vincent St-Amour]

Mon 1/20, Room TBA 1:30-3:00
Aaron

Reasoning about concurrency

Concurrency allows processes to observe and influence each other *as*
they compute, rather than *between* computations.  This
simple-sounding change has radical consequences for programming in and
reasoning about languages.

The talk will start off with a brief discussion on paradigms of
concurrency, and motivate the need for compositional approaches to
concurrency.  We will see both linguistic and logical tools that help
achieve compositionality.  The majority of our time will then be spent
exploring a particular, compositional approach to reasoning about
concurrency, known as Rely/Guarantee.  We'll cover the full R/G logic,
its semantics, its proof of soundness -- and we'll apply it to a
nontrivial concurrent program.

Time permitting, we may also see one of (1) concurrent separation
logic or (2) message-passing concurrency a la CCS & pi-calculus.