In this talk, we introduce the syntax and semantics of Differential Linear Logic. We explain how its rules relate to Linear Logic's rules, and give informal intuitions in terms of functions and distributions. We show how its cut-elimination rules are a reflection of basic calculus rules. We also review Differential Lambda-calculus, with matching intuitions. At the end of the talk, we briefly review two recent development about Differential Linear Logic, in terms of Laplace transformation and co-promotion.[-]

Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.[-]

We consider the Lambek calculus extended with intersection (meet) operation. For its variant which does not allow empty antecedents, Andreka and Mikulas (1994) prove strong completeness w.r.t. relational models (R-models). Without the antecedent non-emptiness restriction, however, only weak completeness w.r.t. R-models (so-called square ones) holds (Mikulas 2015). Our goals are as follows. First, we extend the calculus with the unit constant, introduce a class of non-standard R-models for it, and prove completeness. This gives a simpler proof of Mikulas' result. Second, we prove that strong completeness does not hold. Third, we extend our weak completeness proof to the infinitary setting, to so-called iterative divisions (Kleene star under division).[-]

In this programmatic talk, we will sketch both a conceptual and formal framework for reasoning about the notion of algorithm. This framework will arise from the analysis we will make of the relationships existing between the notion of algorithm and other similar (but still different) notions, like that of computation and that of program. We will first show that the Turing-Church thesis concerning effective computability is not sufficient to capture the notion of algorithm, as it identifies programs which are intensionally different. We will then show the limits of the existing models of computation in capturing some basic construction processes that we are willing to call algorithmic. In order to solve this problem, we propose a formalisation of the notion of model of computation on the base of which we claim that the notion of algorithm could eventually be analyzed. This approach centered around the dynamics of program execution, reconciles the more mechanical view of computation (such as formalized by Turing machines and automata) with the logical view - as it in particular stems from a generalization of Jean-Yves Girard's Geometry of Interaction programme.[-]