No.050 Software Contracts for Communication, Monitoring, and Security

The talk covers three topics related (in my opinion) to 
the seminar: behavioral types, resource usage verification (or typestate
checking), and higher-order model checking, and discuss their relationship.
First, I review our earlier work on behavioral types, and
explain how they can be used for analysis of concurrent programs 
and resource usage verification (or, typestate checking) of functional programs.
I will then explain how that line of work has evolved to our more
recent work on resource usage verification based on higher-order 
model checking.