BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Framework for Specification\, Prototyping\, and Reasoning - Andr
 ew Gacek (University of Minnesota)
DTSTART:20090302T124500Z
DTEND:20090302T140000Z
UID:TALK17163@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:This talk focuses on the specification of and reasoning about 
 formal\nsystems such as type assignment and evaluation semantics in\nprogr
 amming languages. I introduce a logic which allows key aspects of\nsuch sy
 stems\, including variable binding structure within the objects\nthey deal
  with\, to be specified directly and which allows reasoning to\nbe perform
 ed over these specifications. Many of these reasoning tasks\ninductively a
 nalyze the structure of terms by instantiating bound\nvariables with fresh
  free variables. I show how this can be captured\nin a logical setting thr
 ough a process of moving binding from the term\nlevel to the proof level. 
 It is often necessary in reasoning to be\nable to identify occurrences of 
 variables captured by such proof level\nbinders and to be able to distingu
 ish between variable occurrences\ngoverned by different binders. I describ
 e a new logical device that is\ncapable of capturing such rich properties 
 about binding\, and I show\nhow this device can naturally encode informal 
 arguments based on free\nvariable occurrences. Stepping back\, I show how 
 many similar features\nof specifications can be abstracted out by using an
  intermediate\nspecification logic. I briefly describe how this intermedia
 te\nspecification logic can be given an operational semantics so that\nspe
 cifications can be animated automatically\, and I explain how the\nspecifi
 cation logic can be exploited during reasoning to yield many\ninteresting 
 theorems "for free". Finally\, I discuss the implementation\nof these idea
 s in the Abella theorem proving system and describe the\napplications of i
 t that I have explored thus far.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR