ABSTRACT. We present a declarative and modular specification of an automated trading system (ATS) in the concurrent linear framework CLF. We implemented it in Celf, a CLF type checker which also supports executing CLF specifications. We outline the verification of a representative property of trading systems using generative grammars, an approach to reasoning about CLF specifications.

ABSTRACT. Species of structures were first introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics. In 1988, Girard introduced normal functors as a model of pure lambda-calculus where terms are interpreted as infinite series with sets as coefficients (which correspond to a special case of Joyal's species). Fiore presented a generalized definition that both encompasses Joyal's species and constitutes a model of differential linear logic.

Since species encode families of labelled structures, much work has been done to investigate their connection with algebraic data types. We want to explore an alternative viewpoint of seeing them as terms in an extension of lambda-calculus motivated by the relationship between species and differential models of linear logic and use the combinatorial intuition as a guide in the design of the syntax. The next step would be to study methods of resolution of differential equations in the setting of generalized species with the ultimate goal being to establish in linear logic a combinatorial interpretation of the obtained differential calculus.

ABSTRACT. We present a translation from Multiplicative Exponential Linear Logic to a simply-typed lambda calculus with cyclic sharing. This translation is derived from a simple observation on the Int-construction on traced monoidal categories. It turns out that the translation is a mixture of the call-by-name CPS translation and the Geometry of Interaction-based interpretation.

ABSTRACT. In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton’s Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should view this logic as composed of two logics; one sitting to the left of the other. On the left, there is intuitionistic linear logic, and on the right is a mixed commutative/non-commutative formalization of the Lambek calculus. Then both of these logics are connected via a pair of monoidal adjoint functors. An exchange modality is then derivable within the logic using the adjunction between both sides. Thus, the adjoint functors allow one to pull the exchange structural rule from the left side to the right side. We then give a categorical model in terms of a monoidal adjunction, and then a concrete model in terms of dialectica Lambek spaces.

ABSTRACT. In this talk we want to present the recent results of \cite{DK}. We construct several smooth classical denotational models of Linear Logic: they are smooth as non-linear proofs are interpreted as infinitely differentiable functions, and they feature an involutive linear negation. The starting point of this work consists in noticing that the multiplicative disjunction $\parr$ corresponds to the well-known Schwartz' epsilon product. Requiring its associativity then asks for a completeness notion, while the linear involutive negation is ensured by considering a good topology (the Arens topology) on the dual, ensuring that the linear involutive negation works as an orthogonality relation.

ABSTRACT. Process calculi based in logic, such as πDill and CP, provide a foundation for deadlock-free concurrent programming. However, there is a mismatch between the structures of operators used as proof terms in previous work, and the term constructs of the standard π-calculus. We introduce the Hypersequent Classical Processes (HCP), which addresses this mismatch. The key insight is to register parallelism in the typing judgements using hypersequents, a technique from logic which generalises judgements from one sequent to many. This allows us to take apart the term constructs used in Classical Processes (CP) to more closely match those of the standard π-calculus. We prove that HCP enjoys subject reduction and progress, and prove several properties relating it back to CP.

ABSTRACT. Affine lambda-terms are lambda-terms in which each bound variable occurs at most once and linear lambda-terms are lambda-terms in which each bound variable occurs once and only once. In this paper we count the number of affine closed lambda-terms of size n, linear closed lambda-terms of size n, affine closed beta-normal forms of size n and linear closed beta-normal forms of size n, for several measures of the size of lambda-terms. From these formulas, we show how we can derive programs for generating all the terms of size n for each class. The foundation of all of this is a specific data structure, made of contexts in which one counts all the holes at each level of abstractions by lambda's.

ABSTRACT. In this paper, we investigate how to introduce dependent types into the substructural calculi such as the Lambek calculus and linear logic. The motivations of such a move include facilitating a closer correspondence between syntax and semantics in natural language analysis and developing promising applications such as that to concurrency through dependent session types.

We shall present two substructural calculi with dependent types: the first containing dependent Lambek types and the second dependent linear types. Technically, the former adheres to the usual assumption that types do not depend on substructural variables (in this case, the Lambek variables), which makes the technical development easier, while the latter allows type dependency on linear variables, which makes the development more challenging as well as more interesting in applications.

ABSTRACT. This paper studies the so-called generalized multiplicative connectives of linear logic, focusing on the question of finding the ``non-decomposable'' ones, i.e., those that may not be expressed as combinations of the default binary connectives of multiplicative linear logic, Tensor and Par. In particular, we concentrate on generalized connectives of a surprisingly simple form, called ``entangled connectives'', and prove a characterization theorem giving a criterion for identifying the decomposable (resp., undecomposable) entangled connectives.

ABSTRACT. We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the Bang Calculus, a paradigmatic functional language with an explicit box-operator that allows both the call-by-name and call-by value lambda-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value lambda-calculi from both a syntactic and a semantic point of view.

ABSTRACT. We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic. The models thus obtained are finite with respect to several aspects (finite graphs, finite generation of types) and thus improve in this way previous constructions by Seiller. We also discuss how the added notion of coherence can also be used to introduce non-determinism.

ABSTRACT. Semantic evaluation has proven to be a valuable tool to prove computational complexity results on monomorphic type systems. Can we apply it in presence of impredicative polymorphism? The linearity and stratification at work in light logics might make it possible.

ABSTRACT. Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well- established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we seek to start a discussion of benchmarks for Girard’s linear logic and some of its variants. For some quick bootstrapping of the collection of problems, we use translations of the collection of Kleene’s intuitionistic theorems in the traditional monograph Introduction to Metamathematics. We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using linear logic based provers with focusing.

ABSTRACT. We introduce the functional language IQu which, under the paradigm “quantum data & classical control” and in accordance with the model QRAM, allows to define and manipulate quantum circuits and quantum states on which we can execute partial measurement. IQu tailors a lot of ideas from the design of Idealized Algol (roughly, PCF extended with local stores and assignment) and its side-effect management. These ideas play a crucial role in the language design: each quantum co-processor is formalized by means of a quantum register (storing a quantum state) that can be modified by quantum directives (lists of unitary gates). The linearity of quantum states is assured by a one-to one correspondence between quantum states and quantum registers. We adapt the type system of Idealized Algol for typing both quantum-registers and quantum-directives. The types for quantum registers are parametric on the number of qubits and their linearity is granted for free. IQu operates on quantum circuits as they were classical data so no restriction exists on their duplication.

ABSTRACT. We propose to return to the construction carried precedently, where we claimed that Simply-typed approximations = intersection types derivations in the precise sense that we built a categorical equivalence between specific type systems (that encompass all well-known intersection type systems used to characterize normalization) and simply-typed approximations, that we realize as approximation functors, that arise from the translation of the language into linear logic. By studying these specific functors, we claim that their main feature is that they map the exponential of linear logic into what can reasonably be called a resource modality, corresponding either to linear, affine or cartesian intersection types. So, we present the story under the slightly different, and less syntactic, slogan: Intersection type system = multiplicative linear logic + resource modality These resource modalities are linked with well-know systems. In particular, generalized species of structure can be seen as a strictification of the Kleisli category of the linear resource modality. The study of the link between these different resource modality can shed a new light on the extensional collapse, and paving the way for a study of this collapse for dynamic semantics (such as the Geometry of Interaction and ordered combinatory algebras, used to account for forcing and realizability).

ABSTRACT. Finding lower bounds in complexity theory has proven to be an extremely difficult task. Nowadays, only one research direction is commonly acknowledged to have the ability to solve current open problems, namely Mulmuley's Geometric Complexity Theory programme. Relying on heavy techniques from algebraic geometry, it stemmed from a first lower bound result for a variant of Parallel Random Access Machines.

We analyse this original proof, together with two other proofs of lower bounds from a semantics point of view, interpreting programs as graphings -- generalizations of dynamical systems. We show that, abstracted to a more general setting that exploits the classic notion of topological entropy, this three proofs share the same structure. This reformulation recentres the proofs around dynamical aspects, relegating the use of algebraic geometry to a model-driven choice rather than a key concept of the method.

ABSTRACT. Proof nets provide permutation-independent representations of proofs and are used to investigate coherence problems for monoidal categories. We investigate a coherence problem concerning Second Order Multiplicative Linear Logic MLL2, that is, the one of characterizing the equivalence over proofs generated by the interpretation of quantifiers by means of ends and coends. By adapting the "rewiring approach" used in the proof net characterization of the free *-autonomous category, we provide a compact representation of proof nets for a fragment of MLL2 related to the Yoneda isomorphism. We prove that the equivalence generated by coends over proofs in this fragment is fully characterized by the rewiring equivalence over proof nets.

ABSTRACT. We show that the normal form of the Taylor expansion of a λ-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier’s original proof along three independent directions.

First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad-hoc.

We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables.

Finally, we extend all the results to a non-deterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier’s approach can be preserved in this setting.