BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A call-by-value realizability model for PML - Rodolphe Lepigre\, L
 aboratoire de Mathématiques\, Université de Savoie
DTSTART:20160226T140000Z
DTEND:20160226T150000Z
UID:TALK64148@talks.cam.ac.uk
CONTACT:Ohad Kammar
DESCRIPTION:We present a new type system with support for proofs of progra
 ms in a\ncall-by-value language with control operators. The proof mechanis
 m relies\non observational equivalence of (untyped) programs. It appears i
 n two type\nconstructors\, which are used for specifying program propertie
 s and for\nencoding dependent products. The main challenge arises from the
  lack of\nexpressiveness of dependent products due to the value restrictio
 n. To\ncircumvent this limitation we relax the syntactic restriction and o
 nly\nrequire equivalence to a value. The consistency of the system is obta
 ined\nsemantically by constructing a classical realizability model in thre
 e\nlayers (values\, stacks and terms).\n
LOCATION:SS03
END:VEVENT
END:VCALENDAR