[Pl-seminar] Semantics Seminar Schedule
Mitchell Wand
wand at ccs.neu.edu
Tue Nov 4 00:05:01 EST 2008
NU Programming Languages Seminar
Wednesday, November 5, 2008
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
RCF, Refinement Types, and the State Monad
Riccardo Pucella
NU PRL
Abstract:
RCF [Bengtson, Bhargavan, Fournet, Gordon, and Maffeis, 2008] is a
concurrent lambda-calculus equipped with refinement types for
expressing pre- and post-conditions within first-order logic. The
values of a refinement type {x:T | C} are the values of the type T
that satisfy the formula C. Refinement types are a way of unifying
type systems with program logics. The goal of RCF is to verify
security properties of the source code of cryptographic protocols and
access control mechanisms. Well-typed programs enjoy assertion-based
security properties, with respect to a realistic threat model
including key compromise. But RCF is a calculus that is useful beyond
its ability to establish security properties.
I will spend most of the talk reviewing RCF and talking about
refinement types. I will also describe work that Andy Gordon and I
started this summer on using RCF as a basis for capturing stateful
type systems. As an example, I will consider the problem of
typechecking stateful (role-based) access control properties, where
the set of permissions of the code depends on the roles that are
active at runtime.
================================================================
Upcoming Events:
# Wed 11/12 no seminar
# Wed 11/19 Geoffrey Mainland (Harvard): Flask: Functional Programming
for sensor networks (tentative)
# No talks scheduled past these. Come give a talk!
--Mitch
More information about the pl-seminar
mailing list