A refinement of the state monad

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

• Johannes Borgstrom (MSR Cambridge)
• Monday 23 November 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• de239's list

Note that ex-directory lists are not shown.