2022 Joint Workshop

Linearity & TLLA

 

Haifa, Israel
31 July - 1 August 2022

 

Affiliated with FSCD and LICS at FLOC 2022

 

Submit

Linearity & TLLA 2022 is the 3rd edition of the Joint International Workshop on Linearity and Trends in Linear Logic and its Applications.

Aims

The workshop aims at bringing 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. Linearity is a key feature in both theoretical and practical approaches to computer science, and the goal of this workshop is to present work exploring linearity both in theory and practice. Addressed topics include proof representation, operational, static and dynamical models of programming languages, linear languages and type systems, parallelism and concurrency, quantum and probabilistic computation, as well as philosophy and linguistics.

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. Linearity and 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:

  • LL methods in the theory of programming languages;
  • categorical models of proofs and programs;
  • dynamical models of computations, games and languages;
  • linear term calculi;
  • linear type systems;
  • linear proof-theory;
  • linear programming languages;
  • implicit complexity;
  • sub-linear logics;
  • parallelism and concurrency;
  • interaction-based systems;
  • verification of linear systems;
  • quantum and probabilistic models of computation;
  • biological and chemical models of computation;
  • linguistics;
  • logic and philosophy.

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=tllalinearity2022

Important Dates

All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
  • Submission: 20 May 2022 3 June 2022
  • Notification: 17 June 2022 24 June 2022
  • Final version: 1 July 2022
  • Workshop: 31 July - 1 August 2022

Invited speakers

  • Stephanie Balzer - Carnegie Mellon University
    Recursive Session Logical Relations
    Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types — but exclusively for terminating languages. In this talk, I develop a logical relation for an intuitionistic linear logic session type language with general recursive types and instantiate it for proving progress-sensitive noninterference. Concurrency and non-termination pose several challenges, and I explain how the logical relation addresses them. A distinguishing feature of the development is the choice of an observational step index, which ensures compositionality and proofs of transitivity and soundness.
  • Thomas Ehrhard - CNRS and Paris Cité University
    A coherent differential PCF
    The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite non-determinism and indeed these languages are essentially non-deterministic. Based on a recently introduced categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces, this talk will present a deterministic version of the differential lambda-calculus. One nice feature of this new approach to differentiation is that it is compatible with general fixpoints of terms, so our language is actually a differential extension of PCF.
  • Giulio Guerrieri - Huawei-Edinburgh Joint Lab
    The Call-by-Value Lambda-Calculus from a Linear Logic Perspective
    Plotkin's call-by-value (CbV, for short) lambda-calculus is a variant of the lambda-calculus that models the evaluation mechanism in most functional programming languages. The theory of the CbV lambda-calculus is not as well studied as the call-by-name one, because of some technical issues due to the "weakness" of Plotkin's CbV beta-rule, which leads to a mismatch between syntax and semantics. By adopting a Curry-Howard perspective, we show how linear logic inspires several ways to solve the mismatch between syntax and semantics in CbV, paving the way for restoring a theory of the CbV lambda-calculus as elegant as the one for call-by-name. We test our approach on a type-theoretic/semantic characterization of normalizabilty and on the notion of solvability.

Programme

All schedules are given in Haifa local time; see also the programme on the FLOC easychair site.

Sunday July 31st

  • 14h00-14h30 Welcome
  • 14h30-15h30 Stephanie Balzer (invited speaker) - Recursive Session Logical Relations
  • 15h30-16h00 Pause
  • 16h00-16h30 Marie Kerjean, Jean-Simon Lemay - Copromotion and Taylor Approximation
  • 16h30-17h00 Davide Barbarossa - Denotational semantics driven simplicial homology
  • 17h30-17h30 Rémi di Guardia, Olivier Laurent - Bottom-up sequentialization of unit free MALL proof-nets

Monday August 1st

  • 09h30-10h30 Thomas Ehrhard (invited speaker)- A coherent diffential PCF
  • 10h30-11h00 Pause
  • 11h00-11h30 Jean-Baptiste Joinet - Dissymetrical Linear Logic
  • 11h30-12h00 Siva Somayyajula - Parametric Chu Translation
  • 12h00-12h30 Matteo Manighetti, Dale Miller - Peano Arithmetic and muMALL: An extended abstract
  • 12h30-14h00 Pause
  • 14h00-15h00 Giulio Guerrieri (invited speaker) - The Call-by-Value Lambda-Calculus from a Linear Logic Perspective
  • 15h30-16h00 Anderson Beraldo-de-Araujo - Cloning and deleting quantum information from a linear logical point of view

Program Committee

Chairs

Members

 

Organising Committee

  • Sandra Alves - University of Porto, Portugal
  • Thomas Ehrhard - IRIF, University of Paris, France
  • Stefano Guerrini - LIPN, University Sorbonne Paris Nord, France
  • Lorenzo Tortora de Falco - University Roma Tre, Italy
  • Daniel Ventura - Federal University of Goiás. Brasil