~~NOCACHE~~
/* DO NOT EDIT THIS FILE */
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 14 décembre 2023, 10 heures 30, ENS Lyon\\
**Marianna Girlando & Sonia Marin, Paige Randall North, Lionel Vaux Auclair** //Séminaire CHOCOLA//
\\
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 7 décembre 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Meven Lennon-Bertrand** (Université de Cambridge) //Towards a certified proof assistant kernel – What it takes and what we have//
\\
Proof assistant kernels are a natural target for program certification:
they are small, critical, and well-specified. Still, despite the
maturity of the field of software certification, we are yet to see a
certified Agda, Coq or Lean. In this talk, I will try and explain why
this is not such an easy task, and present two complementary projects
going in that direction. The first, MetaCoq, is a large scale project,
broadly aiming at giving tools to manipulate Coq terms and derivations
inside of Coq, in particular developing an important body of formalized
proofs around Coq's typing. The second is a more recent endeavour, aimed
at tackling the mother of all properties: normalisation.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 23 novembre 2023, 10 heures 30, Salle 3052\\
**Luca Reggio** (University College London) //Games, comonads, and categorical homotopy//
\\
The game comonads research programme, started by Samson Abramsky and Anuj Dawar in 2017, provides categorical accounts of key constructions in finite model theory, and has led to an axiomatic approach to various notions of logical resources central to this field.
I will outline some preliminary ideas on how to bring the tools of homotopy theory to the research area of game comonads, with the aim of tackling open questions concerning e.g. expressive completeness and preservation results.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 16 novembre 2023, 10 heures 30, ENS Lyon\\
**Morgan Rogers, Cyril Cohen, Simon Forest** (Various institutions) //Séminaire CHOCOLA//
\\
Joint session with the CHOCOLA seminar. See details at:
https://chocola.ens-lyon.fr/events/meeting-2023-11-16/
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 9 novembre 2023, 10 heures 30, Salle 3052\\
**Andreas Nuyts** (KU Leuven) //Multimodal Type Theory and Applications//
\\
Certain properties of (type) dependencies in typed programming languages can be established syntactically by observing non-violation, shortcutting the need of a manual proof. Examples of such properties are variance, irrelevance, parametricity, or causality as in guarded type theory. A type system where function types are annotated with a *modality* expressing the function's behaviour, can account for this syntactic check as part of type-checking. From the need to type basic function operations, we find that these modalities should have the structure of an ordered monoid, or more generally they can be the morphisms of a 2-category whose objects are called *modes*. The purpose of multi[mode/modal] type theory (MTT) is to provide a type system, parametrized by a 2-category called the *mode theory* which abstractly achieves this result.
After introducing MTT and its models, depending on the timing and the interests and background of the audience, we can either look at questions arising during the implementation of MTT, or at applications. Some applications that I have worked on, or am working on, are Degrees of Relatedness (for parametricity & irrelevance), naturality type theory (naturality & variance), and the modal transpension system (for internalizing aspects of presheaf models). J. Ceulemans' Sikkel library for Agda explores how MTT can help to use the many extensions of type theory found in the literature *locally and modularly*.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 19 octobre 2023, 10 heures 30, Salle 3052\\
**Tba** //Séminaire CHOCOLA//
\\
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 12 octobre 2023, 10 heures 30, Salle 3052\\
**Juliusz Chroboczek** (Université Paris Cité) //Le routage next-hop : une introduction illustrée sur le protocole Babel//
\\
L'Internet est un réseau consistant de plusieurs dizaines de milliards de
nœuds. Le *routage* est le problème d'acheminer un paquet à travers un
réseau. Le paradigme de routage utilisé dans l'Internet s'appelle le
*routage next-hop*.
Dans cet exposé, je ferai une introduction au routage next-hop, puis je
décrirai comment il est traditionnellement réalisé dans l'Internet. Je
décrirai les faiblesses des techniques traditionnelles de routage, et je
montrerai comment le protocole de routage Babel vise à les contourner.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 28 septembre 2023, 10 heures 30, Lyon\\
**Antoine Allioux, Liseau Blondeau-Patissier, William Simmons** //Séminaire CHOCOLA//
\\
Titles and abstracts available at:
https://chocola.ens-lyon.fr/events/meeting-2023-09-28/
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 21 septembre 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Brigitte Pientka** (McGill University) //A Layered Modal Type Theory For Meta-Programming -- Where Meta-Programming Meets Intensional Code Analysis//
\\
Metaprogramming is the art of writing programs that produce or
manipulate other programs. This opens the possibility to eliminate
boilerplate code and exploit domain-specific knowledge to build
high-performance programs. While this widely used concept is almost as
old as programming itself, it has been surprisingly challenging to
extend to logical frameworks and type-theory in general.
In this talk, I present a layered modal type theory that provides a logical
foundation to meta-programming with intensional code analysis.
At its core (layer 0), has a pure (simply-typed) calculus with no
modality. Layer 1 is obtained by extending the core with one layer of
contextual box types which describes open code at layer 0 and supports pattern
matching on open code from layer 0. Although both layers fundamentally
share the same language and the same typing judgment, we only allow
computation at layer 1. As a consequence, layer 0 accurately
captures the syntactic representation of code in contrast to the
computational behaviors at layer 1. The system is justified by
normalization by evaluation (NbE) using a presheaf model.
The normalization algorithm extracted from the model is sound and complete
and is implemented in Agda.
We see this work as a stepping stone towards developing a dependent type
theory that supports intensional code analysis in meta-programming.
This is joint work with Jason Z. Hu.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 22 juin 2023, 10 heures 30, Room: TBA\\
**Hall Hands On Deck** //AG//
\\
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Vendredi 26 mai 2023, 9 heures 30, Amphi 9e Halle aux Farines\\
**All Hands On Deck** (PPS pole) //Journées PPS 2023//
\\
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 25 mai 2023, 9 heures 30, Amphi 9e Halle aux Farines\\
**All Hands On Deck** (pole PPS) //Journées PPS 2023//
\\
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 13 avril 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Giulio Manzonetto** (Université Sorbonne Paris Nord) //The Lambda Calculus - 40 Years Later//
\\
Barendregt's book "The Lambda Calculus, its syntax and
semantics" (1981/84) has become a `classic' in Theoretical Computer
Science because it presents the state of the art in lambda calculus
in a comprehensive way, and proposes a number of open problems and
conjectures.
In 2022, Barendregt and Manzonetto published a `sequel'
of this book, presenting the solutions of several of these problems,
and more. In this talk, we will present a selection of these problems
and the key ingredients that were employed to solve them.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 30 mars 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Romain Pascual** (Université Paris-Saclay) //Graph transformation for reasoning about geometric modeling operations//
\\
Topology-based geometric modeling deals with the representation of nD objects,
which splits the topological description, i.e., the representation of the objects'
topological cells (vertices, edges, faces, volumes, ...), and the geometric
information, i.e., the addition of data to the topological cells. We study the
combinatorial models of generalized and oriented maps represented as attributed
typed graphs subject to consistency conditions.
This representation allows the study of modeling operations as graph rewriting
rules. The motivation is twofold. First, we study the preservation of the model
consistency through syntactic conditions statically checked on the rules. Second,
we extend rules into rule schemes to abstract over the underlying topology.
This formalization of modeling operations also offers guidelines for inferring
operations from a representative example consisting of an initial and a target
object. The inference mechanism is implemented in Jerboa, a platform for designing geometric modelers exploiting graph transformation rules.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 23 mars 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Giulio Manzonetto** //Postponed to Apil 13th.//
\\
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 16 mars 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Adrien Durier** (Université Paris-Saclay) //Open call-by-value and concurrency//
\\
Milner's work on functions as processes shows how the
evaluation strategies of the lambda-calculus can be faithfully mimicked
in the pi-calculus, allowing a dynamic representation of functional
programs. Milner namely studies the call-by-name and call-by-value
evaluation strategies, and raises the problem of full abstraction for
these encodings, i.e., what are the equivalences induced by these
encodings. The theory of call-by-name is well-studied and understood,
and the problem of full abstraction for call-by-name was solved shortly
after. On the other hand, the theory of call-by-value on open terms is
complex, and we present the solution of the full abstraction problem for
call-by-value, which was left open until quite recently.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 9 mars 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Ghyselen Alexis** (Università di Bologna) //Choices via algebraic operations and stateful computations//
\\
Algebraic operations, as defined by Plotkin and Power, are well-studied and powerful tools to provide denotational semantics for computational lambda-calculus and it is especially useful in design for abstraction of effectful computations, allowing a high degree of modularity by separating effect signatures from their interpretations. The practical counterpart of this is obtained by the use of handlers, a popular tool in functional programming that can actually provide concrete implementations of effect signatures while preserving modularity.
In this talk, I will present a joint work with Ugo Dal Lago and Francesco Gavazzo on how algebraic operations, and handlers, can support decision-making abstractions in functional programs: a user can invoke an operation to resolve choices without implementing the underlying selection mechanism, and can give feedback by way of rewards. We differ from some recently proposed approach to the problem based on the selection monad, by Abadi and Plotkin, as we express the underlying selection mechanism with efficient algorithms implemented by a set of handlers. I will first introduce algebraic effects and handlers, then present the selection monad approach for choices, and our approach, based on stateful computations (or equivalently comodels). Both the theoretical and practical aspects will be examined, and I will show the practical efficiency of our approach compared to the selection monad. Finally, I will focus on how our work can actually be implemented in a modular way on a concrete language with handlers and how we can use expressive type systems to obtain safety properties, especially ensuring a high-degree of modularity and a sound usage of algebraic operations.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 23 février 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Francesco Gavazzo** (University of Pisa) //Computational Effects From a Relational Angle//
\\
Program execution rarely happens in isolation. Indeed, during its evaluation a program may modify the memory of the machine, interact with external processes, change the flow of the computation, etc. All these phenomena are known as computational effects, and they can be informally described as those side effects happening during the evaluation process of the program.
Computational effects are of paramount importance to understand program behaviour, and indeed they are one of the main research topics in programming language semantics since the very birth of the discipline. Starting with the seminal work by Eugenio Moggi, computational effects have been successfully understood relying on the language of algebra and category theory, with notions such as monad, algebraic (and Lawvere) theory, and distributive law being nowadays well-accepted idioms in the programming language community.
Although the categorical perspective on computational effects has been particularly effective to model the denotational semantics of effectful programs it does not work so well when it comes to accounting for their operational behaviour. In this talk, I will introduce the theory of computational effects by first reviewing the categorical approach to effectful programs, focusing in particular on Plotkin and Power's theory of algebraic effects, and then moving to computational effects in (some subfields of) operational reasoning. In particular, I will give evidence that by extending the aforementioned categorical notions from a categorical (functional) to an allegorical (relational) setting, it is possible to obtain an elegant operational theory of computational effects having the same level of generality as its denotational counterpart.
To maintain the talk as accessible as possible, I will give a first introductory part on computational effects and then move to the more technical relational development. The latter will consist of a general high-level outline of the results achieved in the context of operational reasoning and of a more in-depth case study.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Mardi 14 février 2023, 11 heures, Salle 3052 & online ([[https://u-paris.zoom.us/j/86981929910?pwd=SGd1dVI5ODZiU0tKZzdOZ3NPWE1Idz09]|Zoom link]])\\
**Benoît Valiron** (CentraleSupélec) //Complete Equational Theories for Linear Optical and Quantum Circuits//
\\
In this talk, we introduce two complete equational theories:
one for linear optical circuits and one for quantum circuits. More
precisely, in both cases we introduce a set of circuit equations that
we prove to be sound and complete: two circuits represent the same
quantum evolution if and only if they can be transformed one into the
other using the equations.
We shall first present our proposed equational theory for linear
optical circuits. We shall then discuss how the semantics of both
kind of circuits differ, and how to relate them using
controlled-gates. The discussion will drive is to the completeness
result for quantum circuits, based on the one for linear optical
circuits.
Joint session with the Algorithmes et complexité seminar series.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 9 février 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Clément Blaudeau** (INRIA Paris, CAMBIUM Project-Team) //Retrofitting OCaml modules//
\\
ML modules are offer large-scale notions of composition and modularity. Provided
as an additional layer on top of the core language, they have proven both vital
to the working OCaml and SML programmers, and inspiring to other use-cases and
languages. Unfortunately, their meta-theory remains difficult to comprehend, and
more recent extensions (abstract signatures, module aliases) lack a complete
formalization. Building on a previous translation from ML modules to Fω, we
propose a new comprehensive description of a significant subset of OCaml
modules, including both applicative and generative functors and the proposed
feature of transparent ascription. By exploring the translations both to and
from Fω, we provide a complete description of the signature avoidance issue, as
well as insights on the limitations and benefits of the path-based approach of
OCaml type-sharing.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 26 janvier 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**George Metcalfe** (University of Bern) //Deciding equations in ordered groups and ordered monoids//
\\
(Joint work with Almudena Colacito, Nikolaos Galatos, and Simon Santschi)
This talk will be about deciding equations in various classes of ordered groups and ordered monoids, and how this relates to deciding if there exist orders on free groups and monoids satisfying finitely many inequalities.
Removing the inverse operation from any lattice-ordered group (l-group) yields a distributive lattice-ordered monoid (l-monoid), but not every distributive l-monoid admits a group structure. Indeed, every distributive l-monoid is a (possibly finite) pointwise-ordered monoid of order-preserving maps on a chain, whereas every l-group is a pointwise-ordered group of order-preserving permutations on a chain and must be either trivial or infinite.
We will see that the equational theory of distributive l-monoids is decidable and coincides with the equational theory of l-groups without inverses, and hence, by eliminating inverses, that the equational theory of l-groups is also decidable. This contrasts with the fact that there are inverse-free equations that are satisfied by all totally ordered abelian groups but not all totally ordered commutative monoids, and the decidability of the equational theory of the latter is open.
[[seminaires:pps:index|Preuves, programmes et systèmes]]\\
Jeudi 12 janvier 2023, 10 heures 30, Salle 3052 & online ([[https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09|Zoom link]])\\
**Rémy Cerda** (Université d'Aix-Marseille) //Taylor expansion for the infinitary λ-calculus//
\\
Ehrhard and Regnier’s Taylor expansion of λ-terms has been broadly used as an approximation theory for several variants of the λ-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree.
We extend this framework to the (001-)infinitary λ-calculus, where terms and reductions may be infinite, and where the normal forms are precisely the Böhm trees. This enables us to give a unified presentation of the Commutation theorem, thanks to the simulation of the infinitary reduction by the (finitary, confluent and terminating) reduction of the Taylor expansion.
Finally we deduce new, simple proofs of confluence and genericity for the infinitary λ-calculus, as well as approximation-based characterisations of head- and β-reductions.
Corresponding paper (submitted to LMCS): https://arxiv.org/abs/2211.05608.
This is joint work with my supervisor Lionel Vaux Auclair (I2M, AMU).