8th International Workshop on
Trends in Linear Logic and Applications

TLLA 2024

 

Tallinn, Estonia
8-9 July 2024

 

Affiliated with FSCD 2024

 

Program

Photo by Karson on Unsplash

TLLA 2024 is the 8th edition of the International Workshop on Trends in Linear Logic and its Applications.

Aims

The workshop aims at bringing together researchers who are currently developing theory and applications of linear logic as a technical tool or a methodological guideline, to foster their interaction and provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area. Linear Logic is a key feature in both theoretical and practical approaches to computer science, and the goal of this workshop is to present work exploring the theory of Linear Logic so as its applications.

Motivation

Ever since Girard's linear logic (LL) was released, there has been a stream of research where linearity is a key issue, covering both theoretical topics and applications to several areas of Mathematical Logic and Computer Science, such as work on proof representation and interpretations (proof nets, denotational semantics, geometry of interaction etc), complexity classes (including implicit complexity), programming languages (especially linear operational constructs and type systems based on linear logic), and more recently probabilistic and quantum computation, program analysis, expressive operational semantics, and techniques for program transformation, update analysis and efficient implementation. The foundational concepts of LL also serve as bridges to other topics in mathematics of course (functional analysis, categories) as well as to linguistics and philosophy.

Topics of Interest

New results that make central use of linearity, ranging from foundational work to applications in any field, are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental questions about existing theories and practices. Topics of interest include, but are not limited to:

  • theory of programming languages
  • games and languages
  • proof theory
  • categories and algebra
  • implicit computational complexity
  • parallelism and concurrency
  • quantum and probabilistic computing
  • models of computation
  • possible connections with combinatorics
  • functional analysis and operator algebras
  • philosophy of logic and mathematics
  • linguistics

Submission

Contributions are not restricted to talks presenting original results, but are also open to tutorials, open discussions, and position papers. For this reason, we strongly encourage contributions presenting work in progress, open questions, and research projects. Contributions presenting the application of linear logic results, techniques, or tools to other fields, or vice versa, are most welcome.

To propose a contributed talk submit a short abstract whose length is between 2 and 5 pages on

      https://tlla-2024.sciencesconf.org

The abstracts of the contributed and invited talks will be published on the site of the conference.

Important Dates

All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
  • Submission: 15 May 2024 22 May 2024
  • Notification: 25 May 2024 31 May 2024
  • Final version: 14 June 2024
  • Workshop: 8-9 July 2024

Invited speakers

  • Giulio Manzonetto - IRIF, France
    Coloring Intersection Types
    We review the key findings on intersection type systems by comparing two main approaches: the qualitative analysis of termination properties and the quantitative evaluation of resource consumption. We will expose the relationship between the underlying systems of approximants, based on Böhm trees and Taylor expansions, and observational equivalences. We will then introduce the ``yinyang calculus'', an annotated lambda-calculus that allows to track the interaction between a lambda-term and its environment. By appropriately coloring an intersection type system, we prove that the usual Böhm tree equality can be characterized in terms of a quantitative equivalence where we observe the termination in a certain number of interaction steps.
  • Pierre-Marie Pédrot - INRIA, Rennes
    Dialectica The Ultimate
    Since the seminal work of De Paiva, it is well-known that Gödel's Dialectica interpretation has strong ties with linear logic. This construction has many close relatives that are ubiquitary in the construction of models of LL, e.g. Chu spaces and double glueing. As a matter of fact, Dialectica can be seen as a way to computationally track the uses of contraction and weakening in a term, and is therefore a very natural way to add a linear content to an otherwise intuitionistic system. How expressive and general is it, exactly? Are all models of LL at risk of being subsumed by some form of Dialectica interpretation? In this talk, we will give some evidence that the tide is rising. We will recall not only how Dialectica scales to Martin-Löf type theory, using a variant of a recent model by Moss-von Glehn, but also that it can be seen as a higher-order, dependently-typed generalization of both graded monads and Atkey's Quantitative Type Theory.

Tutorials

  • Davide Barbarossa - Bath University, UK
    Differential aspects of the approximation theory of the lambda-calculus
    In this tutorial, we will study the notion of approximation for the lambda-calculus. After having introduced the topic, we will focus on the so-called "resource approximation" and use it in order to prove the Continuity Lemma for the lambda-calculus. We will then see how this approximation technique is actually related to the notion of differentiation in the lambda-calculus on the one hand, and how it provides an abstraction of the usual notion of differentiation from mathematical analysis on the other hand, by looking (time permitting) at its categorical formulation.
  • Nobuko Yoshida - Oxford, UK
    Session types, Linear Logic and Expressiveness
    Session types are a type discipline to specify and verify communications through protocol descriptions. It has been already 30 years since the first paper on session types, by Kohei Honda at CONCUR 1993. This talk first gives an origin of session types, and then shows the expressiveness results based on the development of a Curry-Howard correspondence with linear logic developed by Caires, Pfenning, Perez, Toninho and others. It concludes with a different kind of expressiveness, related to choice behaviours of session types.

Program

(schedules are given in CEST)



July 8

09:00
Welcome
09:15
Invited Talk
Pierre-Marie Pédrot. Dialectica The Ultimate.
10:00
Coffee break
10:30
3. Mikołaj Bojańczyk, Lê Thành Dũng Nguyễn, Rafał Stefański. Function spaces for orbit-finite sets.
10:55
11:20
Short break
11:40
12:05
7. Jacopo Furlan. The art of realizability.
12:30
Lunch
14:00
Tutorial
Nobuko Yoshida. Session types, Linear Logic and Expressiveness.
15:30
Coffee break
16:00
16:25
4. Antonio Bucciarelli, Raffaele Di Donna, Lorenzo Tortora de Falco. Injectivity of the coherent model for a fragment of connected MELL proof-nets.
16:50
17:15
Closure


July 9

09:15
Tutorial (first part)
Davide Barbarossa. Differential aspects of the approximation theory of the lambda-calculus.
10:00
Coffee break
10:30
Tutorial (second part)
Davide Barbarossa. Differential aspects of the approximation theory of the lambda-calculus.
11:15
11:40
Short break
11:45
Invited Talk (joint ITRS)
Giulio Manzonetto. Coloring Intersection Types.
12:30
Lunch
14:00
8. Wesley Fussner, Simon Santschi. Interpolation in extensions of linear logic.
14:25
14. Niccolò Veltri, Cheng-Syuan Wan. Craig interpolation for semi-substructural logics.
14:50
Short break
15:00
15:30
Coffee break
16:00
16:25
16:50
Closure

Program Committee

Chairs

Members

 

Organising Committee

  • Thomas Ehrhard - IRIF, University of Paris, France
  • Stefano Guerrini - LIPN, University Sorbonne Paris Nord, France
  • Paolo Pistone - Université Lyon 1, France
  • Lorenzo Tortora de Falco - University Roma Tre, Italy