Photo by Daniil Korbut on Unsplash
TLLA 2026 is the 10th edition of the International Workshop on Trends in Linear Logic and its Applications.
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.
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.
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:
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://submissions.floc26.org/tlla
The abstracts of the contributed and invited talks will be published on the site of the conference.
Abstract. The Taylor expansion of a lambda term allows us to approximate its
(possibly infinite) behavior via a sum of ressource terms; likewise
a strategy in game semantics can be seen as a sum of augmentations
(plays up to Mellies's homotopy equivalence).
Typed resource terms are in relation with strategies in games semantics;
more precisely, there is a bijection between normal, eta-long resource
terms and augmentations (up to isomorphism) in Pointer Concurrent Games;
and there is a sound interpretation of the resource calculus in PCG.
However this correspondence relies on the extensionality of the typed
resource calculus -- what happens when we consider a pure calculus,
and what does it mean in terms of extensionality?
We define an extensional version of the (pure) resource calculus,
along with a corresponding extensional Taylor expansion.
This allows us to extend the typed correspondence to an untyped setting:
there is a bijection between normal extensional ressource terms and
augmentations (up to iso) in the universal arena.
This is a first step to study the compositional relationship between
Taylor expansion and game semantics.
(This talk is based on Extensional Taylor Expansion, TheoretiCS 2026,
with Pierre Clairambault and Lionel Vaux Auclair; and on ongoing work.)
Abstract. TBA
Abstract. Substructural logics and languages are central to modelling resource-sensitive computation, such as concurrent processes, memory management, or foundations for quantum programming. Yet, their mechanization in proof assistants remains technically challenging. In this talk, I will focus on mechanizing a core fragment of the quantum programming language Proto-Quipper. I will start by introducing a rational reconstruction of Proto-Quipper languages for static quantum circuit generation. It uses a linear lambda-calculus to describe quantum circuits with normal forms that closely correspond to box-and-wire circuit diagrams. We then show how to integrate this circuit language within a linear/non-linear functional language. This lets us reconstruct Proto-Quipper's circuit programming abstractions using more primitive adjoint-logical operations. This reconstructed version of Proto-Quipper not only allows us to use standard techniques to proof meta-theoretic properties, but it also allows us elegantly mechanize these properties in the Beluga proof environment. This will serve as a instructive example to highlight challenges and lessons learned when it comes to mechanizing substructural systems.
This is joint work with Chuta Sano (McGill) and Ryan Kavanagh (UQAM)
Abstract. Intersection types, since their introduction about fifty years ago, have been known to characterize several normalization properties of $\lambda$-terms via typability. When the intersection operator is made non-idempotent, as first observed by Daniel de Carvalho, intersection types acquire a quantitative flavor, making it possible to capture the cost of normalization of the underlying $\lambda$-term in the Krivine Abstract Machine. Over the last decade, this result has been generalized in several directions. These include evaluation strategies beyond call-by-name, abstract machines beyond the KAM, and alternative calculi, in particular extensions of the $\lambda$-calculus with control operators and effects. At the same time, alternative notions of cost have been investigated, allowing type systems to account not only for time complexity, but also for space consumption. In this tutorial, we present these developments within a unifying framework, focusing in particular on effects, interactive abstract machines, and computation space.
(schedules are given in WEST)
| 09:00 |
Tutorial joint with ITRS
Quantitative Typing Across Effects, Machines, and Notions of Cost. |
| 10:30 |
Coffee break
|
|
Session 1
|
|
| 11:00 | |
| 11:25 | |
| 11:50 | |
| 12:15 | |
| 12:40 |
Lunch
|
| 14:00 |
Invited Talk
Brigitte Pientka. Mechanizing Substructural Systems: Challenges and Lessons Learned. |
|
Session 2
|
|
| 15:00 |
A. Szafarczyk, P. Baillot.
From linear types to relational higher-order logic for analyzing program sensitivity.
|
| 15:25 |
Coffee break
|
|
Session 3
|
|
| 16:00 |
J. Jaramillo, D. Mazza, J. Pérez.
A Linear Logic for Fixpoints and Deadlock Freedom in the Pi-Calculus.
|
| 16:25 | |
| 16:50 |
| 09:00 |
Invited Talk joint with Galop
Hugo Paquet. Concurrency in linear and non-linear game semantics. |
| 10:00 |
Coffee break
|
|
Session 4
|
|
| 10:30 | |
| 10:55 | |
|
Session 5
|
|
| 11:25 | |
| 11:50 | |
| 12:15 |
M. Smykalla, T. Uustalu, N. Veltri, C. Wan.
Multicategories and representability for substructural intuitionistic modal logics.
|
| 12:40 |
Lunch
|
| 14:00 |
Invited Talk
Lison Blondeau-Patissier. Game Semantics of Extensional Taylor Expansion. |
|
Session 6
|
|
| 15:00 |
U. Lago, G. Fiorillo, P. Pistone.
Generating Functions for Probabilistic Programs via the Weighted Relational Model of Linear Logic.
|
| 15:25 |
Coffee break
|
|
Session 7
|
|
| 16:00 | |
| 16:25 | |
| 16:50 |
A. Díaz-Caro, M. Ivnisky, O. Malherbe.
Syntactic linearity and Linear hyperdoctrines for second-order intuitionistic Linear Logic.
|