BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &\; Semantics for Dummies
SUMMARY:Linear Logic - Hugo Paquet (University of Cambridg
e)
DTSTART;TZID=Europe/London:20160205T110000
DTEND;TZID=Europe/London:20160205T120000
UID:TALK63832AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/63832
DESCRIPTION:In maths\, a hypothesis can be used as many times
as needed: if A\nis true\, and A => B is true\, th
en B is true\, but A is still true\nafter that. Th
ings are different in real life. For example\, if
A\nis to spend £1 on apples\, and B is to get them
\, then you lose £1\nin the process and you cannot
do it again.\n\nLinear logic is a refinement of i
ntuitionistic and classical logic\,\nwhich takes t
his into account by forbidding the duplication and
\ndisposal of some hypotheses. This is interesting
on the proof-\ntheoretical side\, but it is also
very relevant to computer science\,\nwhere we need
to reason about the consumption of resources (e.g
. time\, memory).\nLinear logic has therefore been
very influential in the study\nof programming lan
guages\, leading in particular to game semantics\,
\nand to a range of denotational semantics for lan
guages with\nprobabilistic or quantum features.\n\
nI will introduce the syntax of linear logic\, whi
ch involves two\nnew connectives for AND\, two for
OR\, and a unary operator "!"\nindicating which h
ypotheses we are allowed to duplicate or discard.\
nIf I have time\, I will mention some well-known m
odels of linear logic\,\nand present a categorical
axiomatisation of these models.\n\nCovering:\n\n
* The connectives of linear logic and their meani
ng\n * The linear sequent calculus\n * Some mode
ls of linear logic\n * Categorical semantics\n\nI
will only assume a *basic* understanding of\n\n
* Classical and intuitionistic logics\n * Sequent
calculus and Curry-Howard correspondence\n * Cat
egory theory
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
CONTACT:Ian Orton
END:VEVENT
END:VCALENDAR