Events and news relevant to the Laboratory for Foundations of Computer Science

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

We'll have an LFCS seminar today, as part of Nachi's modal logic series:

  Thursday, 03 Sep, 4.10pm
  (Note unusual day)
  Tarmo Uustalu, Reykjavik University

  The seminar will take place in-person only.

A reminder that Tarmo is visiting until Sep 7 (Mon), so please contact him or 
Nachi if you'd like to meet with him.

We're synchronising the seminar time with the teaching timetable, and
plan to start the talk at the advertised time, so please arrive a minute or 
two
earlier.


In detail:

----------------------------------------------------------------------
Tarmo Uustalu, Reykjavik University
https://cs.ioc.ee/~tarmo/

  Thu, 03 Sep, 4.10pm
  Venue: Appleton Tower AT 2.14 (note unusual place and day)



Title: Substructural intuitionistic modal logics, sequent calculi, 
multicategories and representability

Abstract

This is a talk on the structural proof theory of substructural
intuitionistic modal logics defined by categorical semantics. We
will consider substructural intuitionistic versions of K, T, K4 and S4
with multiplicative verum, conjunction and a box modality. We take
them to be defined by semantics in terms of monoidal categories with a
strong monoidal endofunctor, a copointed endofunctor, a semicomonad
or a comonad, optionally (quasi-)idempotent.

I will show that these logics admit elegant cut-free sequent calculi
where the antecedent of a sequent is a list of formulae labelled by
natural numbers for box-depths. The equations governing the
categorical models all translate into eta- and commutative
conversions. With focusing, we achieve subcalculi that keep exactly
one representative of each equivalence class of proofs, allowing us to
easily see that the (quasi-)idempotent variants of these logics enjoy
Mac Lane type coherence: their free models are thin.

I will also demonstrate that the designs of these sequent calculi are
directly justified by equivalent semantics of these logics in terms of
representable multicategories for suitable notions of
(generalized) multicategory and representability: they are
presentations of the free such representable multicategories.

I will briefly discuss adding linear implications.

This is joint work with Michel Smykalla, Niccolò Veltri and
Cheng-Syuan Wan.


----------------------------------------------------------------------

Upcoming events:
----------------
07 Sep (Mon): Gordon Plotkin's 80th birthday celebration
  https://events.inf.ed.ac.uk/plotkin80/
08 Sep (Tue): LFCS's 40th anniversary celebration
  https://events.inf.ed.ac.uk/lfcs40/
09 Sep (Wed): Philip Wadler's 70th birthday celebration
  https://events.inf.ed.ac.uk/wadler70/


Upcoming seminars:
------------------
14 Sep (Mon): Danel Ahman, University of Tartu: A deeper dive into combining 
graded monads and
        graded modal types for temporal resource management

15 Sep: Pranshu Gaba, Tata Institute of Fundamental Research, Mumbai: 
Sure-Almost-Sure
        Window Mean Payoff in Markov Decision Processes



If you would like to propose a speaker, or speak yourself, please contact me.
The seminar webpages:
http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,
Ohad.
The University of Edinburgh is a charitable body, registered in Scotland, 
with registration number SC005336. Is e buidheann carthannais a th’ ann an 
Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.