COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

## Linear LogicAdd to your list(s) Download to your calendar using vCal - Hugo Paquet (University of Cambridge)
- Friday 05 February 2016, 11:00-12:00
- Rainbow Room (FS07), Computer Laboratory.
If you have a question about this talk, please contact Ian Orton. In maths, a hypothesis can be used as many times as needed: if A is true, and A => B is true, then B is true, but A is still true after that. Things are different in real life. For example, if A is to spend £1 on apples, and B is to get them, then you lose £1 in the process and you cannot do it again. Linear logic is a refinement of intuitionistic and classical logic, which takes this into account by forbidding the duplication and disposal of some hypotheses. This is interesting on the proof- theoretical side, but it is also very relevant to computer science, where we need to reason about the consumption of resources (e.g. time, memory). Linear logic has therefore been very influential in the study of programming languages, leading in particular to game semantics, and to a range of denotational semantics for languages with probabilistic or quantum features. I will introduce the syntax of linear logic, which involves two new connectives for AND , two for OR, and a unary operator ”!” indicating which hypotheses we are allowed to duplicate or discard. If I have time, I will mention some well-known models of linear logic, and present a categorical axiomatisation of these models. Covering: - The connectives of linear logic and their meaning
- The linear sequent calculus
- Some models of linear logic
- Categorical semantics
I will only assume a - Classical and intuitionistic logics
- Sequent calculus and Curry-Howard correspondence
- Category theory
This talk is part of the Logic & Semantics for Dummies series. ## This talk is included in these lists:Note that ex-directory lists are not shown. |
## Other listsTest de ligne de prière Rainbow Interaction Seminars Faculty of Economics## Other talksCANCELLED-Open tools in Marchantia for plant bioengineering work and as a platform for elucidating morphogenesis Nuclear fuel manufacture at Westinghouse Springfields past, present and future 'Nobody comes with an empty head': enterprise Hindutva and social media in urban India Making a Crowdsourced Task Attractive: Measuring Workers Pre-task Interactions |