Show simple item record

dc.contributor.authorCuvillier, T
dc.date.accessioned2020-05-22T15:59:33Z
dc.date.issued06/11/2019
dc.identifier.urihttps://qmro.qmul.ac.uk/xmlui/handle/123456789/64298
dc.descriptionPhD thesisen_US
dc.description.abstractMore than 30 years after the discovery of linear logic, a simple fully-complete model has still not been established. As of today, models of logics with type variables rely on di-natural transformations, with the intuition that a proof should behave uniformly at variable types. Consequently, the interpretations of the proofs are not concrete. The main goal of this thesis was to shift from a 2-categorical setting to a first-order category. We model each literal by a pool of resources of a certain type, that we encode thanks to sorted names. Based on this, we revisit a range of categorical constructions, leading to nominal relational models of linear logic. As these fail to prove fully-complete, we revisit the fully-complete game-model of linear logic established by Melliès. We give a nominal account of concurrent game semantics, with an emphasis on names as resources. Based on them, we present fully complete models of multiplicative additive tensorial, and then linear logics. This model extends the previous result by adding atomic variables, although names do not play a crucial role in this result. On the other hand, it provides a nominal structure that allows for a nominal relationship between the Böhm trees of the linear lambda-terms and the plays of the strategies. However, this full-completeness result for linear logic rests on a quotient. Therefore, in the final chapter, we revisit the concurrent operators model which was first developed by Abramsky and Melliès. In our new model, the axiomatic structure is encoded through nominal techniques and strengthened in such a way that full completeness still holds for MLL. Our model does not depend on any 2-categorical argument or quotient. Furthermore, we show that once enriched with a hypercoherent structure, we get a static fully complete model of MALL.en_US
dc.language.isoenen_US
dc.publisherQueen Mary University of London
dc.subjectElectronic Engineering and Computer Scienceen_US
dc.subjectInteractive and Cognitive Environmentsen_US
dc.subjectwearable technologiesen_US
dc.subjectfirst-person visionen_US
dc.titleNominal Models of Linear Logicen_US
dc.typeThesisen_US
dc.rights.holderThe copyright of this thesis rests with the author and no quotation from it or information derived from it may be published without the prior written consent of the author


Files in this item

Thumbnail

This item appears in the following Collection(s)

  • Theses [4223]
    Theses Awarded by Queen Mary University of London

Show simple item record