[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

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