~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[seminaires:sms:index|La syntaxe rencontre la sémantique]]\\
Jeudi 6 mars 2025, 13 heures 30, Salle 3052\\
**Giulio Manzonetto** (IRIF, UPC) //Ohana trees - no variable gets left behind or forgotten//
<button type="link" size="xs" collapse="b31-4559">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b31-4559" collapsed="true">
<well size="sm">
Although the λI-calculus is a natural fragment of the
λ-calculus, obtained by forbidding the erasure, its equational
theories did not receive much attention. The reason is that all proper
denotational models studied in the literature equate all
non-normalizable λI-terms, whence the associated theory is not very
informative. Our goal is to introduce a previously unknown theory of
the λI-calculus, induced by a notion of evaluation trees that we call
‘Ohana trees’. The Ohana tree of a λI-term is an annotated version of
its Böhm tree, remembering all free variables that are hidden within
its meaningless subtrees, or pushed into infinity along its infinite
branches. We develop the associated theories of program approximation:
the first approach is based on finite trees and continuity, the second
adapts Ehrhard and Regnier’s Taylor expansion.
</well>
</collapse>


[[seminaires:sms:index|La syntaxe rencontre la sémantique]]\\
Jeudi 23 janvier 2025, 13 heures 30, Salle 3052\\
**Gabriele Tedeschi** (Univ. Pisa) //Modelling Quantum Protocols: a Novel Semantics with Quantum Probabilities//
<button type="link" size="xs" collapse="b31-4560">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b31-4560" collapsed="true">
<well size="sm">
Quantum protocols involve a number of features like concurrent execution, quantum primitives, message communication and non-determinism. The well-studied calculi and models for probabilistic concurrent systems seem inadequate in the quantum setting, as they do not comply with the observational limitations of quantum theory. We will explore a new semantic model made of "Quantum Distributions" and "Quantum Transition Systems", instead of probability distributions and probabilistic LTSs. We provide a symbolic, quantum semantics for a minimal quantum process calculus, which we prove sound and complete with respect to the known ground, probabilistic behaviour of quantum processes.
</well>
</collapse>


[[seminaires:sms:index|La syntaxe rencontre la sémantique]]\\
Jeudi 16 janvier 2025, 13 heures 30, Salle 3052\\
**Gaëtan Lopez** (IRIF, UPC) //A Rewriting Theory for Quantum λ-Calculus//
<button type="link" size="xs" collapse="b31-4561">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b31-4561" collapsed="true">
<well size="sm">
Quantum lambda calculus has been studied mainly as an idealized programming language—the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus is standardization and normalization results.
</well>
</collapse>