University of Birmingham > Talks@bham > Lab Lunch > Denotational Semantics of Linear Logic with Least and Greatest Fixpoints

Denotational Semantics of Linear Logic with Least and Greatest Fixpoints

Add to your list(s) Download to your calendar using vCal

  • UserFarzad Jafarrahmani, ENS Cachan
  • ClockThursday 09 May 2019, 12:00-13:00
  • HouseCS 217.

If you have a question about this talk, please contact Dr Steve Vickers.

We develop a denotational semantics of full propositional classical linear logic extended with least and greatest fixpoints of formulae (\mu LL) in coherence spaces with totality. The presence of totality predicates, which are a denotational account of the syntactic notion of normalization, allows for dual and non-trivial denotational interpretations of the mu and nu fix point operators involving Knaster Tarski’s theorem. We illustrate the construction by means of several examples such as integer numbers system, and by an embedding of Gödel’s system T. This specific denotational semantics of muLL is clearly an instance of a more general pattern. We also encode the exponentials of linear logic using least and greatest fixpoints and then explain the difference between the new exponentials and the original ones from denotational semantics point of view. This is based on joint work by Thomas Ehrhard.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.