University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > A refinement of the state monad

A refinement of the state monad

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

Behavioural type and effect systems regulate properties such as adherence to object and communication protocols, dynamic security policies, avoidance of race conditions, and many others. Typically, each system is based on some specific syntax of constraints, and is checked with an ad hoc solver.

Instead, we advocate types refined with first-order logic formulas as a basis for behavioural type systems, and general purpose automated theorem provers as an effective means of checking programs.

To illustrate this approach, we give type systems for two related notions of permission-based access control: stack inspection and history-based access control. These type systems are both instances of a refined state monad.

Our main technical result is a safety theorem stating that no assertions fail when running a well-typed program.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity