~~NOCACHE~~
/* DO NOT EDIT THIS FILE               */
/* THIS FILE WAS GENERATED             */
/* EDIT THE FILE "indexheader" INSTEAD */
/* OR ACCESS THE DATABASE              */

{{page>.:indexheader}}

\\ ==== Next talks ====
[[en:seminaires:sms:index|Syntax Meets Semantics]]\\
Thursday May 2, 2024, 2PM, Salle 3071\\
**Mariana Milicich** (IRIF, Universite Paris Cite) //Hybrid Intersection Types for PCF//
<button type="link" size="xs" collapse="b31-4114">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b31-4114" collapsed="true">
<well size="sm">
I will present a type system based on non-idempotent intersection types for PCFh, a variant of PCF. Evaluation in PCFh is hybrid: call-by-name (CBN) and call-by-value (CBV) behaviours cohabit together. Specifically, function application follows CBV semantics, while recursion has a CBN flavour.
This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFh evaluation. This means not only that typability implies normalisation, but also that the converse holds. Moreover, the type system is quantitative, since the size of typing derivations provides upper bounds for the length of normalisation sequences. By refining this type system, we obtain a tight type system, which offers exact information regarding the length of normalisation sequences.
</well>
</collapse>


[[en:seminaires:sms:index|Syntax Meets Semantics]]\\
Thursday June 6, 2024, 2PM, Salle 3071\\
**Adrienne Lancelot** (LIX Polytechnique and IRIF UPC) //Mirroring Call-by-Need, or Values Acting Silly//
<button type="link" size="xs" collapse="b31-4115">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b31-4115" collapsed="true">
<well size="sm">
Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value.

We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need -- that is, its operational equivalence with call-by-name -- showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
</well>
</collapse>


[[en:seminaires:sms:index|Syntax Meets Semantics]]\\
Thursday June 20, 2024, 2PM, Salle 1020\\
**Victor Arrial** (IRIF, Universite Paris Cite) //The Benefits of Diligence//
\\


\\ ==== Previous talks ====
\\ === Year 2024 ===

{{page>.:sms2024}}

\\ === Year 2023 ===

{{page>.:sms2023}}

\\ === Year 2022 ===

{{page>.:sms2022}}