5th International Workshop on
Trends in Linear Logic and Applications

TLLA 2021

 

Online (Rome virtually)
27-28 June 2021

 

Affiliated with LICS 2021

 

Photo by Julius Silver from Pexels

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

Aims

The aim of this workshop is to bring together researchers who are currently developing theory and applications of linear calculi or use 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.

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 (and 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 linear logic or derived tools, 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. The purpose is to gather researchers interested in the connections between Linear Logic and various topics such as:

  • theory of programming languages;
  • categorical models of proofs and programs;
  • dynamical models of computations, games and languages;
  • term calculi;
  • type systems;
  • proof theory;
  • implicit computational complexity
  • parallelism and concurrency
  • interaction-based systems;
  • system and program verification;
  • models of computation;
  • quantum and probabilist models of computation;
  • biological and chemical models of computation;
  • linguistics;
  • logic and philosophy;
  • connections with combinatorics;
  • categories and algebra;
  • functional analysis and operator algebras.

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.

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

Submission is through the Easychair website:
         https://easychair.org/conferences/?conf=tlla2021

Important Dates

All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
  • Submission: 13 May 2021
  • Notification: 31 May 2021
  • Final version: 18 June 2021
  • Workshop: 27-28 June 2021

Invited speakers

  • Marie Kerjean - CNRS - Université Sorbonne Paris Nord, France
    ∂ is for Dialectica
    Dialectica is a proof transformation acting of intuitionnistic logic which factors through Girard's translation. It allows the realization of several semi-classical axioms such as Markov's principle, and the Independence of premises. By taking the viewpoint of differential lambda-calculus and recent developments in differentiable programming, we will show how Dialectica computes higher-order backward differentiation. We will illustrate this through the lens of categories, computation and logic. This is joint work with Pierre-Marie Pédrot.
  • Willem Heijltjes - University of Bath, UK
    The Functional Machine Calculus
    Linear Logic was born out of the Curry-Howard correspondence, from a decomposition of the semantics of the typed lambda-calculus. Over the decades it has proved a valuable tool in the semantic study of computation, where linearity is a common phenomenon. This holds in particular for the areas of computational effects and of concurrency. However, linearity is so abundant, and it occurs in forms that are sufficiently varied, that as yet we do not have a single, complete picture of linear logic as computation. This talk will not solve that. In fact, it will contain very little Linear Logic. Instead, it will present a simple and natural account of effectful computation, the Functional Machine Calculus (FMC). The calculus suggests a new perspective the Curry-Howard correspondence, and thus on the foundations of linear logic, and raises more questions than it answers. But it might just present a way forward in our understanding of linear logic and computation. The FMC itself consists of two generalizations to the lambda-calculus. One is to parameterize abstraction and application in a set of 'locations', similar to the channels of process calculi. This will allow to encode effectful operations for state and input/output, via the standard interpretation of application and abstraction as push and pop actions in an abstract machine. The other is to generalize the variable construct with a restricted continuation. This naturally includes composition and identities in the calculus and allows to express reduction behaviour such as CBN and CBV. The calculus is then confluent. Semantically it corresponds to Hasegawa's kappa-calculus, Power and Thielecke's closed Freyd categories, and Hughes's arrows for Haskell.
  • Beniamino Accattoli - Inria-Saclay, France
    A Reasonable Presentation of IMELL
    Linear logic is usually presented via the sequent calculus, but it operational theory is then developed via proof nets, because the sequent calculus is considered inadequate, due to its many commutative cases of cut elimination. Here we follow a new alternative approach, in the intuitionistic setting. We attach proof terms to the sequent calculus for IMELL, and, inspired by Accattoli and Kesner's linear substitution calculus, we endow them with special rules for cut elimination avoiding commutative cases. For such an IMELL substitution calculus, we develop a solid operational theory from scratch---namely, proving untyped confluence, typed strong normalization, and untyped normalization for a new strategy---via neat and direct proofs organized around basic principles. We then show that the new strategy has the subterm property of abstract machines and that its number of steps is a reasonable time cost model, the first such results in the linear logic literature.

Tutorials

  • Lionel Vaux - Université d’Aix-Marseille, France
    Proof nets
    Proof nets can be referred to as 'the natural deduction of Linear Logic'. They provide a graphical syntax for proofs, quotienting out the irrelevant permutations of rules from the sequent calculus. They moreover allow to define cut elimination locally, without the need for commuting conversions. We will start by presenting proof nets for the multiplicative fragment MLL (without units), in which the theory is most satisfactory. Then we will extend the approach to the multiplicative-exponential fragment, and show how cut elimination in MELL proof nets allows to refine the β-reduction of the λ-calculus into finer steps. We will conclude with a brief survey of more recent contributions involving proof nets.
  • Matteo Acclavio - Université du Luxembourg
    An introduction to combinatorial proofs
    Combinatorial proofs are a graphical syntax that can be used to provide a notion of proof equivalence for classical logic. They have been proposed by Hughes 15 years ago to address Hilbert's 24th problem, that is, how to identify the simplest proof for a statement. In recent years this syntax has been developed, and now provides a notion of proof equivalence for a wide family of logics.  In this tutorial we focus on combinatorial proofs for classical logic. We shall present the key features of this syntax, and then analyse the notion of proof equivalence it enforces in various proof systems. We will conclude the tutorial with an overview of the state of the art of combinatorial proofs, providing intuitions on how the combinatorial syntax can be extended and refined to express proofs for logics such as relevant, modal and intuitionistic logic.

The abstracts of the contributed talks are available at the HAL repository.

Program

(all schedules are given in CEST)

Sunday, June 27th 2021

09:00 - 10:30 TUTORIAL I (Chair: Lorenzo Tortora de Falco)

10:30 - 11:00 Virtual Coffee Break

11:00 - 12:30 TUTORIAL II (Chair: Lorenzo Tortora de Falco)

12:30 - 14:00 Lunch

14:00 - 16:00 Session I (Chair: Thomas Ehrhard)

  • Invited talk - Willem HEIJLTJES (slides).
  • Proof-nets as graphs - Giulio Guerrieri, Giulia Manara, Luc Pellissier, Lorenzo Tortora De Falco and Lionel Vaux Auclair (slides).
  • Principal Types as Lambda Nets - Pietro Di Gianantonio and Marina Lenisa (slides).
  • A gentle introduction to Girard's Transcendental Syntax - Boris Eng and Thomas Seiller (slides).

16:00 - 16:30 Virtual Coffee Break

16:30 - 17:30 Session II (Chair: Giulio Guerrieri)

  • Geometry of Interaction for ZX-Diagrams - Kostia Chardonnet, Benoît Valiron and Renaud Vilmart (slides).
  • Parallelism in Soft Linear Logic - Paulin Jacobé De Naurois
  • Totally Linear Proofs - Victoria Barrett and Alessio Guglielmi

17:30 - 18:30 Special evening lecture: Michele Abrusci - slides (Chair: Christian Retoré)

Monday, June 28th 2021

09:00 - 11:00 Session III (Chair: Elaine Pimentel)

  • Invited talk - Marie KERJEAN (slides).
  • Evaluation and convergence in the computational calculus - Claudia Faggian, Giulio Guerrieri and Riccardo Treglia
  • Toward a Curry-Howard Equivalence for Linear, Reversible Computation - Kostia Chardonnet, Alexis Saurin and Benoît Valiron (slides).
  • Linear Exponentials as Graded Modal Types - Jack Hughes, Daniel Marshall, James Wood and Dominic Orchard (slides).

11:00 - 11:30 Virtual Coffee Break

11:30 - 12:30 Session IV (Chair: Paolo Pistone)

  • On relation between totality semantic and syntactic validity - Thomas Ehrhard, Farzad Jafarrahmani and Alexis Saurin
  • Click and coLLecT: An Interactive Linear Logic Prover - Etienne Callies and Olivier Laurent (slides).
  • A Parametrised Functional Interpretation of Affine Logic- Bruno Dinis and Paulo Oliva (slides).

12:30 - 14:00 Lunch

14:00 - 16:00 Session V (Chair: Lionel Vaux)

  • Invited talk - Beniamino ACCATTOLI: A Reasonable Presentation of IMELL
  • A bunched logic for l^p spaces - June Wunder, Arthur Azevedo de Amorim, Patrick Baillot and Marco Gaboardi (slides).
  • Probabilistic logic programming with multiplicative modules - Roberto Maieli (slides).
  • Towards Unifying (Co)induction and Structural Control - Siva Somayyajula (slides).

16:00 Closing

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