7th International Workshop on
Trends in Linear Logic and Applications

TLLA 2023

 

Rome, Italy
1-2 July 2023

 

Affiliated with FSCD 2023

 

Program

Photo by David Köhler on Unsplash

TLLA 2023 is the 7th 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
  • linguistics

Submission

Contributions are not restricted to talks presenting an original results, but 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.

Authors are invited to submit a short abstract whose length is between 2 and 5 pages. Please include in the abstract the names and the email addresses of all the authors.

Please send your submission to

      tlla23@irif.fr

specifying in the email message the names of the corresponding authors and their email addresses, if different from the sending one, which in any case will be used for further communications.

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 2023 extended to 21 May 2023
  • Notification: 22 May 2023 reported to 26 May 2023
  • Final version: 31 May 2023 reported to 16 June 2023
  • Workshop: 1-2 July 2023

Invited speakers

  • Zeinab Galal - Sorbonne Université, France
    Bicategorical semantics of linear logic with profunctors
    I will present an overview of recent developments in the bicategorical semantics of lambda calculus and linear logic. I will focus in particular on the bicategory of profunctors and the model of generalized species of structures by Fiore, Gambino, Hyland and Winskel.
  • Gabriele Vanoni - INRIA-Sophia Antipolis, France
    Higher-Order Bayesian Networks
    Bayesian networks (BN) are a well-known machine learning model, and are used with profit in many applications. Their theory is well founded on statistics and (algorithmic) stochastic inference. But what do BN represent from a programming language perspective? First, we show that every program written in a linear fragment of probabilistic call-by-push-value lambda calculus is a BN (the converse is trivial). Then, we overcome the linearity constraint on the language, and we prove that all the programs linearly typed correspond indeed to Bayesian networks. This allows for elegant definitions of extensions of BN such as templates BN and recursive BN. Along the way, we provide a factor-based denotational semantics of our language, defined through an intersection type system.

Tutorials

  • Alexis Saurin - Université Paris Cité, France
    A tour of the non-wellfounded linear proof-theory of the mu-calculus: on the virtues of circular reasoning
    TBA
  • Marcelo Fiore - University of Cambridge, UK
    A Potpourri of Hopeful Trends and Applications for and to Linear Logic
    TBA

Program

(schedules are given in CEST)



July 1

09:00
Gabriele Vanoni. Higher-Order Bayesian Networks.
10:00 Coffee break
10:30
1. Antonio Bucciarelli, Raffaele Di Donna, Lorenzo Tortora de Falco. Towards injectivity of the coherent model for connected MELL proof-nets.
10:55
6. Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, Lionel Vaux Auclair. Sequentialization is as fun as bungee jumping.
11:20
4. Flavien Breuvart, Marie Kerjean, Simon Mirwasser. Unifying Graded Linear Logic and Differential Operators.
11:45
15. Matteo Acclavio. Multiplicative Logic Beyond Cographs.
12:10
17. Giulio Guerrieri, Giulia Manara, Lorenzo Tortora de Falco, Lionel Vaux Auclair. Confluence for untyped proof nets via parallel cut elimination .
12:35 Lunch
14:00
Alexis Saurin. A tour of the non-wellfounded linear proof-theory of the mu-calculus: on the virtues of circular reasoning.
15:30 Coffee break
16:30
16. Aurore Alcolei, Luc Pellissier, Alexis Saurin. The exponential logic of sequentialization.
16:55
18. Matteo Acclavio, Gianluca Curzi, Giulio Guerrieri. Non-uniform polynomial time via non-wellfounded parsimonious proofs.
17:20
12. Antonio Veredice. Some notes on the beginning of Linear Logic in Italy.
17:45
11. Marie Kerjean, Valentin Maestracci, Morgan Rogers. Functorial Models of Differential Linear Logic.


July 2

09:00
Zeinab Galal. Bicategorical semantics of linear logic with profunctors.
10:00 Coffee break
10:30
3. Davide Barbarossa, Paolo Pistone. Tropical Mathematics and the Lambda-Calculus.
10:55
9. Valentin Maestracci, Thomas Seiller. Linear Realizability and Cobordisms.
11:20
8. Adrien Ragot, Thomas Seiller, Lorenzo Tortora de Falco. Linear realisability over nets and second order quantification.
11:45
10. Morgan Rogers, Thomas Seiller, William Toiani. Normal functors[ions], [the irrelevence of] power series, and [a new model of] 𝜆-calculus.
12:10
14. Alexander V. Gheorghiu, Tao Gu, David J. Pym. Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic.
12:35 Lunch
14:00
Marcelo Fiore. A Potpourri of Hopeful Trends and Applications for and to Linear Logic.
15:30 Coffee break
16:30
13. Carlos Olarte, Elaine Pimentel. Multi-modalities and non-commutativity in functorial linear logic: a case study.
16:55
2. Miguel Ramos, Riccardo Treglia, Delia Kesner. A Quantitative Understanding of Exceptions.
17:20
7. Anupam Das, Damiano Mazza, Lê Thành Dũng Nguyễn, Noam Zeilberger. On the Complexity of Normalization for the Planar λ-calculus.
17:45
5. Rémy Cerda, Lionel Vaux Auclair. How To Play The Accordion. On the (Non-)Conservativity of the Reduction Induced by the Taylor Approximation of λ-Terms.

Program Committee

Chairs

Members

 

Organising Committee

  • Thomas Ehrhard - IRIF, University of Paris, France
  • Stefano Guerrini - LIPN, University Sorbonne Paris Nord, France
  • Lorenzo Tortora de Falco - University Roma Tre, Italy