Photo by Gabriel McCallin on Unsplash
TLLA 2025 is the 9th 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://tlla2025.sciencesconf.org
The abstracts of the contributed and invited talks will be published on the site of the conference.
Abstract. Gentzen designed his natural deduction proof system to “come as close as possible to actual reasoning.” Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. PSF (Proof Search Framework) attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated. (This talk is based on a paper that appears in LICS 2023.)
Abstract. Dependent Type Theory is inherently computational. Constructions and proofs in Type Theory are programs that can be executed to produce results. However, all these programs and explanations are built with no regard for computational complexity within the theory, meaning that constructions cannot reason or rely on complexity bounds, and arguments that rely on complexity restrictions lie outwith the grasp of Type Theory. To address this, I will talk about combining techniques from Implicit Computational Complexity with Dependent Type Theory to attempt to bring resource consciousness to Type Theory. Systems for implicit complexity often depend on linear typing, so a form of Linear Dependent Types using Quantitative Type Theory will be necessary.
Abstract. TBA
Abstract. TBA
(schedules are given in WEST)
| 08:45 |
Welcome
|
|
| 09:00 |
1.
Rémi Di Guardia.
A Formalization of Multiplicative Proof-Nets in Rocq.
(joint work by Rémi Di Guardia, Olivier Laurent) |
|
| 09:20 |
15.
Matteo Acclavio.
Proof nets for first-order MALL.
(joint work by Matteo Acclavio, Giulia Manara) |
|
| 09:40 |
16.
Raffaele Di Donna.
Proof-nets and the bang calculus.
(joint work by Giulio Guerrieri, Raffaele Di Donna) |
|
| 10:00 |
Coffee break
|
|
| 10:30 |
Invited Talk
Dale Miller. A system of inference based on proof search. |
|
| 11:30 |
6.
Joanna Boyland.
Compiling adjoint natural deduction to the semi-axiomatic sequent calculus.
(joint work by Joanna Boyland, Frank Pfenning) |
|
| 11:50 | ||
| 12:10 |
5.
Elies Harington.
An extensional perspective on higher categorical models of linear logic.
(joint work by Elies Harington, Samuel Mimram) |
|
| 12:30 |
Lunch
|
|
| 14:00 |
Tutorial
Linear / non-linear logic and models of probabilistic, quantum and meta programming. |
|
| 15:30 |
Coffee break
|
|
| 16:00 |
11.
Matteo Acclavio.
Linear logic and choreographic programming.
(joint work by Matteo Acclavio, Giulia Manara, Fabrizio Montesi) |
|
| 16:20 | ||
| 16:40 |
3.
Houssein Mansour.
Amplification Rate of Contextual Distances in Randomised Programming.
Online talk.
(joint work by Houssein Mansour, Raphaëlle Crubillé) |
|
| 17:00 |
20.
Colin Bloomfield.
Very Small Dialectica Categories.
Online talk.
(joint work by Colin Bloomfield, Peter Jipsen, Valeria de Paiva) |
| 09:00 | ||
| 09:20 |
13.
Alexis Saurin.
On a Proof-Relevant Interpolation Theorem for Circular Proofs in Linear Logic.
(joint work by Daniel Osorio-Valencia, Alexis Saurin) |
|
| 09:40 |
17.
Charles Grellois.
Quantitativity and Fixed Points in the Infinitary Relational Semantics of Linear Logic.
(joint work by Pierre Clairambault, Charles Grellois) |
|
| 10:00 |
Coffee break
|
|
| 10:30 |
Invited Talk
Robert Atkey. Implicit Polynomial Time and Linear Dependent Types. |
|
| 11:30 |
9.
Arturo De Faveri.
Exploring Semigroup-Theoretic Techniques in Lambda Calculus.
(joint work by Antonio Bucciarelli, Arturo De Faveri, Giulio Manzonetto, Antonino Salibra) |
|
| 11:50 | ||
| 12:10 |
19.
Jun Suzuki.
Undecidability of Linear Logic without Weakening.
(joint work by Jun Suzuki, Katsuhiko Sano) |
|
| 12:30 |
Lunch
|
|
| 14:00 |
Tutorial
Linearity and Deep Inference. |
|
| 15:30 |
Coffee break
|
|
| 16:00 | ||
| 16:20 |
12.
Daniel Zackon.
Mechanizing linear logical relations.
(joint work by Daniel Zackon, Brigitte Pientka, Alberto Momigliano) |
|
| 16:40 |
14.
Guido Fiorillo.
On Correctness, Sequentialization and Interpolation.
(joint work by Guido Fiorillo, Daniel Osorio Valencia, Alexis Saurin) |
|
| 17:00 |
4.
Malena Ivnisky.
An Algebraic Extension of Intuitionistic Linear Logic: The LS!-Calculus and Its Categorical Model.
(joint work by Alejandro Díaz-Caro, Malena Ivnisky, Octavio Malherbe) |
|
| 17:20 |
Closure
|