View: session overviewtalk overviewside by side with other conferences

08:45 | Modalities and Linearity SPEAKER: Elaine Pimentel ABSTRACT. |

09:45 | The inhabitation problem for non-idempotent intersection SPEAKER: Simona Ronchi Della Rocca ABSTRACT. The inhabitation problem for intersection types is known to be undecidable. We study the problem in the case of non-idempotent intersection, in particular for a type assignment system characterizing solvable terms, and we prove decidability through a sound and complete algorithm. |

10:45 | Undecidability of Multiplicative Subexponential Logic SPEAKER: Kaustuv Chaudhuri ABSTRACT. Subexponential logic is a variant of linear logic with a family of exponential connectives---called subexponentials---that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that classical propositional multiplicative linear logic extended with one unrestricted and two incomparable linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable. |

11:15 | Superstructural Reversible Logic SPEAKER: Zachary Sparks ABSTRACT. Linear logic refines conventional logic by being a ``resource-conscious'' logic. We analyze the notion of resource maintained by linear logic proofs and argue that it only focuses on a ``spatial'' dimension omitting another important ``temporal'' dimension. We generalize (or further refine using even more structural rules) linear logic to maintain combined spatial and temporal resources. The resulting logic is reversible and thus allows a study of reversible computation from a proof-theoretic perspective. |

11:45 | A Linear/Producer/Consumer model of Classical Linear Logic SPEAKER: Jennifer Paykin ABSTRACT. This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions that reflect the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into category theory. The work also presents several concrete instances of the LPC model, including one based on finite vector spaces. |

12:15 | Cut Elimination in Multifocused Linear Logic SPEAKER: unknown ABSTRACT. We study cut elimination for a multifocused variant of linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in the standard focused system, related to the constraints in grouping rule instances inside focusing phases. We show that cut elimination can be performed in a sensible way even though the proof requires specific lemmas to deal with multifocusing phases, and discuss the difficulties arising with cut elimination when considering normal norms of proofs in linear logic. |

14:30 | Continuations, closed reduction and process networks SPEAKER: Ian Mackie ABSTRACT. In the early 1990s it was shown that the linear lambda-calculus |

15:30 | Type Classes for Lightweight Substructural Types SPEAKER: Edward Gan ABSTRACT. Linear and substructural types are powerful tools, but adding them to standard functional programming languages often means introducing extra annotations and typing machinery. We propose a lightweight substructural type system design that recasts the structural rules of weakening and contraction as type classes; we demonstrate this design in a prototype language, Clamp. Clamp supports polymorphic substructural types as well as an expressive system of mutable references. At the same time, it adds little additional overhead to a standard Damas–Hindley–Milner type system enriched with type classes. We have established type safety for the core model and implemented a type checker for Clamp in Haskell. |

16:30 | Ludics without Designs I: Triads SPEAKER: Michele Basaldella ABSTRACT. In this paper, we introduce the concept of triad. Using this notion, we study, revisit, discover and |

17:00 | Wave-Style Token Machines and Quantum Lambda Calculi SPEAKER: unknown ABSTRACT. Particle-style token machines are a way to interpret proofs and programs, when the latter are written following the principles of linear logic. In this paper, we show that token machines also make sense when the programs at hand are those of a simple quantum lambda-calculus. This, however, requires generalizing the concept of a token machine to one in which more than one particle travel around the term at the same time. The presence of multiple tokens is intimately related to entanglement and allows to give a simple operational semantics to the calculus, coherently with the principles of quantum computation. |

17:30 | Geometry of Resource Interaction – A Minimalist Approach SPEAKER: Marco Solieri ABSTRACT. The Resource λ-calculus (RC) is a variation of the λ-calculus where arguments can be superposed and must be linearly used. Hence it is a model for non-deterministic and linear programming languages, and the target language of the Taylor expansion of λ-terms. In a strictly typed restriction of RC, we study the notion of path persistency and we define a Geometry of Interaction inspired by the dynamic algebra. We show that the GoI is invariant under reduction and characterises persistency by means of path regularity. Our construction is also complexity aware, in the sense that it is able to count the non-zero addends in the normal forms a resource term. |

18:00 | A new point of view on the Taylor expansion of proof-nets and uniformity SPEAKER: Giulio Guerrieri ABSTRACT. We introduce (in the multiplicative and exponential fragment of linear logic) the notion of protodifferential net. We then define a coherence relation on the set of proto-differential nets and prove the analogue of the result proven for differential lambda-terms, which does not hold for differential nets: a set of proto-differential nets is the subset of the proto-Taylor expansion of some proof-structure if and only if it is a clique. |