[Pl-seminar] [PL seminar] Stephanie Balzer (CMU) on Nov 13, noon: details

[Artem Pelenitsyn]

Dear all,

This is a reminder that Stephanie's talk will happen this upcoming Friday,
Nov 13, at noon in Zoom
--- join by the desktop app: https://northeastern.zoom.us/j/93707532703
--- join by the browser: https://northeastern.zoom.us/wc/join/93707532703/

Please, schedule a 1-to-1 meeting with Stephanie *by commenting* on a cell
in this spreadsheet
<https://docs.google.com/spreadsheets/d/1s0Q5sUyTxNYkh77u1EDKceoJfAVOKL0HSmDQGNQDJvI/edit?usp=sharing>

--
Best, Artem

On Mon, 26 Oct 2020 at 10:20, Artem Pelenitsyn <a.pelenitsyn at gmail.com>
wrote:

> Dear all,
>
> Three things in this email:
>
> * Please, schedule a 1-to-1 meeting with Stephanie *by commenting* on a
> cell in this spreadsheet
> <https://docs.google.com/spreadsheets/d/1s0Q5sUyTxNYkh77u1EDKceoJfAVOKL0HSmDQGNQDJvI/edit?usp=sharing>
>
> * The seminar talk will take place on November 13, Friday, noon in Zoom:
> --- join by the desktop app: https://northeastern.zoom.us/j/93707532703
> --- join by the browser: https://northeastern.zoom.us/wc/join/93707532703/
>
> * Details of the talk are as follows.
>
> Title: Manifest Deadlock-Freedom for Shared Session Types
>
> Abstract:
>
> Shared session types generalize the Curry-Howard correspondence between
> intuitionistic linear logic and the session-typed pi-calculus with adjoint
> modalities that mediate between linear and shared session types, giving
> rise to a programming model where shared channels must be used according to
> an acquire-release discipline.  The resulting language recovers the
> expressiveness of the untyped asynchronous pi-calculus and accommodates
> practical programming scenarios, such as shared servers, file systems etc.
> The resulting language is implemented as a prototype in C0 (a safe subset
> for C used to teach freshmen at CMU) and as a DSL in Rust [1].
>
> The generalization, however, comes at the cost of deadlock-freedom, a
> property which holds for the purely linear fragment.  In this talk, I
> report on recent work that makes up for this deficiency and introduces a
> type system of linear and shared session types in which the adjoint
> modalities are complemented with possible worlds to rule out cyclic
> dependencies between acquires and synchronizations.  I distill the key
> abstractions to reason about cyclic dependencies and the key invariants
> enforced by the type system to guarantee deadlock-freedom.  Time permitted,
> I report on ongoing work that also uses possible world modalities for
> type-based verification of program properties of interest.
>
> Bio:
>
> Stephanie Balzer [2] is a research faculty in the Principles of
> Programming group in the Computer Science Department at Carnegie Mellon
> University.  Stephanie obtained her PhD from ETH Zurich under the
> supervision of Thomas R. Gross.  In her PhD work, Stephanie developed the
> sequential relationship-based programming language Rumer and an
> invariant-based verification technique for Rumer.  Stephanie’s current work
> focuses on the development of type systems and logics for verifying
> properties of concurrent programs.
>
> References:
>
> [1] https://github.com/maybevoid/ferrite
> [2] http://www.cs.cmu.edu/~balzers/
>
-------------- next part --------------
HTML attachment scrubbed and removed