Logica Matematica Types by Need (joint work with Beniamino Accattoli and Maico Leberle)
Linear Implicative Algebras, a Brouwer-Heyting-Kolmogorov interpretation
of linear logic Giulio Guerrieri
Luc Pellissier
18-01-2019 - 11:00
Largo San Leonardo Murialdo,1 - Pal.C Aula 311 - Terzo piano 1)Giulio Guerrieri
A cornerstone of the theory of λ-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models.
Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type erivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.
2) Luc Pellissier
Implicative Algebras were recently introduced by Alexandre Miquel as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly. In this ongoing work, we show how linear logic fits in this picture: we present a notion of model of intuitionnistic linear logic in which sits both syntactic models and a localized phase semantics ; and show how to transform such a model into an algebra allowing to interpret faithfully all the connectives of classical linear logic.
org: TORTORA DE FALCO Lorenzo
|
