Séminaire, 14 novembre 2013
Programme
- 10:30 – 12:00
-
Dominic Hughes (Stanford)
Linear logic decomposes classical logic into multiplicatives, additives and exponentials. Multiplicative proof nets are remarkably elegant; additive and exponential nets have struggled in comparison. Could this struggle mean that additives and exponentials are simply the wrong way to decompose classical logic?
I present a decomposition of classical first-order logic which retains multiplicatives at its core and replaces additives and exponentials with a naive notion: a function f is the ideal parallel representation of contraction and weakening. Contraction occurs when f(x)=f(y) and weakening occurs outside the image of f.
The approach clarifies the units: the positive multiplicative unit is retained and the three problematic units are rejected. Quantifiers are broadly similar to those in multiplicative proof nets.
[Note: additives and exponentials are interesting and elegant in their own right; here I reject them only from the perspective of decomposing classical first-order logic.]
- 14:00 – 15:00
-
Beniamino Accattoli (Univ. di Bologna)Invited talk: Toward a New Theory of Exponential Proof-Nets
Despite being one of the most successful outcomes of linear logic, the theory of proof-nets for Multiplicative and Exponential Linear Logic (MELL) is not fully satisfactory. In this talk I will discuss two of its shortcomings, the need of explicit boxes, and the elaborated reasoning behind its proof of strong normalization. In the first part I will show how switching to a polarized version of MELL allows to internalize boxes, so that they are induced by the proof itself, instead of being explicitly added to the graph. These "implicit boxes" are canonical and enjoy a correctness criterion which is a natural extension of Laurent's criterion for Polarized MELL. Moreover, they induce new cut-elimination rules.
In the second part I will focus on the new dynamics recasted in the usual, non-polarized setting with explicit boxes. I will introduce a notion of substitution for proof nets and use it to revisit the proof of strong normalization, organizing it along three abstract principles. The new dynamics admits a very simple proof of these principles (and thus of strong normalization), while the ordinary dynamics does not.
- 15:30 – 17:00
-
Neelakantan R. Krishnaswami (Max Planck Institute)Invited talk: Types for Higher-Order Functional Reactive Programming
Functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style.
In this talk, I describe a new language for higher-order reactive programming. This language generalizes and simplifies work on functional reactive programming, supporting the use of higher-order abstractions such as first-class functions and streams of streams.
Furthermore, the type system can be understood (via the Curry-Howard correspondence) as a proof system for a variant of linear temporal logic, and the type discipline also permits a simple and provably efficient implementation strategy.
Time permitting, I will also discuss some preliminary work on denotational models for this calculus.
