TLLA 2021

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

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.

Program Committee

Chairs

• Elaine Pimentel - Federal University of Rio Grande do Norte, Brazil
• Christian Retoré - University of Montpellier, France

Members

• Claudia Faggian - CNRS - University Paris Diderot, France
• Giulio Guerrieri - University of Bath, UK
• Sonia Marin - University College London, UK
• Naohiko Hoshino - Sojo University, Japan
• Paolo Pistone - University of Bologna, Italy
• Myriam Quatrini - Aix-Marseille Université, France
• Thomas Seiller - CNRS - University Sorbonne Paris Nord, France
• Lutz Strassburger - Inria Saclay, France

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