BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Nominal terms and one-and-a-half level Curry-Howard - Jamie Gabbay
DTSTART:20080926T130000Z
DTEND:20080926T140000Z
UID:TALK12174@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:The Curry-Howard correspondence equates propositions with type
 s and\nderivations with lambda-terms.  The lambda-calculus does not\nimmed
 iately provide terms to correspond to _incomplete_\nderivations --- deriva
 tions containing "holes".  Solutions include\nlambda-lifting\; I will show
  how a suitable notion of typed nominal\nterm can also represent incomplet
 e terms and give a nice Curry-Howard\ncorrespondence which very precisely 
 matches what we do when we fill in\na proof on a piece of paper.  The typi
 ng system is quite\nsophisticated\, corresponding with first-order logic.\
 n\nAn overview is as follows:\n* Types correspond with first-order logic p
 redicates.\n* Terms correspond with incomplete proofs.\n* Level 1 variable
 s (atoms) correspond with assumptions\; types of the variables correspond 
 with predicates assumed.\n* Level 2 variables (unknowns) correspond with u
 nknown parts of the derivation.\n* A notion of beta-reduction for level 1 
 variables corresponds with\nproof-normalisation.\n* Instantiation of level
  2 variables corresponds with filling in more of\nthe derivation.\n\nFull 
 details are in "my conference paper\nwith Mulligan":http://www.gabbay.org.
 uk/papers.html#curhid and more information\, including slides of the talk\
 n(before the talk\, if I'm really efficient) can be found "on my homepage"
 :http://www.gabbay.org.uk/.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR