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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

A refinement of the state monad

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Cambridge Arts Picturehouse, St. Andrews Street T001, Department of Materials Science and Metallurgy Seminar Rooms SG1 & 2, Alison Richard Building

Other talks

TBC Gastroenterology and Acute Medicine Title TBC Title abstract tbc Understanding the Interplay between LLMs' Utilisation of Parametric and Contextual Knowledge Clonal haematopoiesis, early detection and pre-leukemia to leukemia development
 

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