BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Linear Logic - Hugo Paquet (University of Cambridge)
DTSTART:20160205T110000Z
DTEND:20160205T120000Z
UID:TALK63832@talks.cam.ac.uk
CONTACT:Ian Orton
DESCRIPTION:In maths\, a hypothesis can be used as many times as needed: i
 f A\nis true\, and A => B is true\, then B is true\, but A is still true\n
 after that. Things are different in real life. For example\, if A\nis to s
 pend £1 on apples\, and B is to get them\, then you lose £1\nin the proc
 ess and you cannot do it again.\n\nLinear logic is a refinement of intuiti
 onistic and classical logic\,\nwhich takes this 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 sc
 ience\,\nwhere we need to reason about the consumption of resources (e.g. 
 time\, memory).\nLinear logic has therefore been very influential in the s
 tudy\nof programming languages\, leading in particular to game semantics\,
 \nand to a range of denotational semantics for languages with\nprobabilist
 ic or quantum features.\n\nI will introduce the syntax of linear logic\, w
 hich involves two\nnew connectives for AND\, two for OR\, and a unary oper
 ator "!"\nindicating which hypotheses we are allowed to duplicate or disca
 rd.\nIf I have time\, I will mention some well-known models of linear logi
 c\,\nand present a categorical axiomatisation of these models.\n\nCovering
 :\n\n  * The connectives of linear logic and their meaning\n  * The linear
  sequent calculus\n  * Some models of linear logic\n  * Categorical semant
 ics\n\nI will only assume a *basic* understanding of\n\n  * Classical and 
 intuitionistic logics\n  * Sequent calculus and Curry-Howard correspondenc
 e\n  * Category theory
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR