[talks] R Dockins general exam

[Melissa Lawson]

Rob Dockins will present his research seminar/general exam on Thursday 
October 16 at 3PM in Room 402.  The members of his committee are:  
Andrew Appel (advisor), David Walker, and Brian Kernighan.  Everyone is 
invited to attend his talk and those faculty wishing to remain for the oral exam 
following are welcome to do so.  His abstract and reading list follow below.
------------------------------------
Title: 
  Modal Separation Logic for Program Verification and Metatheory

Abstract:

  The construction of new logics for reasoning about programs has a
  long history in the field of program verification, going back at
  least to the seminal works of Floyd and Hoare. In this talk, I shall
  show how to combine separation logic with a generic multimodal logic
  using the proof assistant Coq.  The logic that results is useful as
  a substrate for building higher-level program logics and as a tool
  for proving metatheoretic properties.

  The techniques I present can be readily generalized across different
  programming languages and support a large collection of features
  including mutable memory, unstructured control flow, explicit memory
  management, and shared-memory concurrency.  I present examples
  from a toy language, the list machine benchmark, and from
  Concurrent C Minor, a realistic intermediate language for a
  concurrent C compiler.


Reading List:

Books:
Benjamin Pierce. Types and Programming Languages. MIT Press.  2002.
Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development.
  Springer.  2004.
G.E. Hughes and J.M. Cresswell. A New Introduction to Modal Logic.
  Routldge.  1996.

Papers:
Andrew W. Appel, Paul Andre Mellies, Christopher D. Richards
  and Jerome Vouillon.  A Very Modal Model of a Modern, Major,
  General Type System.  In Proc. Thirty-Fourth Annual ACM SIGPLAN 
  Symposium on Principles of Programming Languages (POPL), January 2007.
Chriatian Calcagno, Peter O'Hearn, Hongseok Yang.  Local Action and
  Abstract Separation Logic.  In Proc. Twenty-Second Annual IEEE 
  Symposium on Logic in Computer Science (LICS), July 2007.
Alexy Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky and Mooly Sagiv.
  Local Reasoning for Storable Locks and Threads.  In Proc. Fifth Asian
  Symposium on Programming Languages and Systems (APLAS), November 2007.
Xavier Leroy and Sandrine Blazy. Formal Verification of a C-like Memory Model
  and Its Uses for Verifying Program Transformations.  Journal of Automated
  Reasoning, 41(1):1-31.  July 2008.
Greg Morrisett, David Walker, Karl Crary and Neal Glew. From System F to Typed
  Assembly Language.  Twenty-Fifth ACM SIGPLAN Symposium on Principles of 
  Programming Languages (POPL), January 1998.
Peter O'Hearn. Resources, Concurrency and Local Reasoning.  Theoretical Computer
  Science 375(1):271-307, May 2007.
Vaughan R. Pratt.  Application of Modal Logic to Programming.
  Studia Logica, 39(2-3):257-274.  June, 1980.
John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures.
  In Proc. Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS),
  July 2002.