BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Resolving inductive definitions with binders - Matt Lakin (Univers
 ity of Cambridge)
DTSTART:20090309T124500Z
DTEND:20090309T140000Z
UID:TALK17165@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:We study inductive definitions involving binders\, in which al
 iasing between free and bound names is permitted. Such aliasing occurs in 
 informal specifications of operational semantics\, but is excluded by the 
 common representation of binding as meta-level lambda-abstraction. Drawing
  upon ideas from functional logic programming\, we represent such definiti
 ons with aliasing as recursively defined functions in a higher-order typed
  functional programming language that extends core ML with types for name-
 binding\, a type of "semi-decidable propositions" and existential quantifi
 cation for types with decidable equality. We show that the representation 
 is sound and complete with respect to the language's operational semantics
 \, which combines the use of evaluation contexts with constraint programmi
 ng. We briefly discuss the associated constraint problem\, which is NP-com
 plete\, and outline a constraint solving algorithm.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR