Les types dépendants permettent de rajouter des preuves d'invariants dans les structures de données et ainsi de faire des programmes corrects par construction. L'envers de la médaille est une multiplication des structures subtilement différentes pour lesquelles il faut prouver des lemmes similaires de manière répétée. L'ornementation est un outil méta-théorique introduit par Conor McBride qui permet de décrire ces relations et apporte avec lui une boite à outils de méta-programmation. J'ai étendu cette notion aux types inductifs-récursifs, des définitions simultanées d'une structure et d'un éliminateur. Ceux-ci sont nécessaires pour définir certains gros univers mais apparaissent également ``dans la vie courante''. Je m'attarderai surtout sur des exemples et leur axiomatisation méta- théorique qui a récemment progressée.
La logique de séparation concurrente est un formalisme qui permet de raisonner sur des programmes impératifs (manipulant des pointeurs) et concurrents. Dans cet exposé, je vous donnerai un aperçu des principes généraux sur lesquels est basé le système Iris, développé par Derek Dreyer et ses collaborateurs.
TBA
Recent works have indicated the potential of using curvature as a regularizer in image segmentation, in particular for the class of thin and elongated objects. These are ubiquitous in biomedical imaging (e.g. vascular networks), in which length regularization can sometime perform badly, as well as in texture identification. However, curvature is a second-order differential measure, and so its estimators are sensitive to noise. State-of-art techniques make use of a coarse approximation of curvature that limits practical applications. In this talk I propose the use of multigrid convergent estimators instead, and I will show a new digital curvature flow derived from it that mimics continuous curvature flow. Finally, an application as a post-processing step to a variational segmentation framework is presented.
Cet exposé s'inspire de la connexion remarquée récemment entre les séries formelles et calculs non-commutatifs et qui permet de retrouver très simplements des résultats de Nisan et d'autres sur les calculs non-commutatifs de polynômes. Je présenterai les résultats de base sous l'angle des séries formelles puis je montrerai l'application aux calculs monotones (commutatifs) et les perspectives et difficultés pour utiliser ces techniques pour des modèles avec moins de restrictions.
La sémantique d'un programme est souvent donnée d'une des deux façons suivantes: ou bien comme une fonction mathématique (la fonction qu'il calcule) ou bien par le biais de son execution. La première méthode tend à détruire toute information fine sur le programme (complexité par exemple), alors que la seconde impose un cadre de bas niveau, syntaxique, sans la structure et les propriétés mathématiques donnés par la première. Pour allier les avantages des deux méthodes, de nombreux sémanticiens s'intéressent à représenter les programmes comme des interactions (interactions qui se déroulent entre un programme et son contexte); ceci en permet une compréhension dynamique. Le lambda-calcul est un formalisme standard pour représenter les programmes fonctionnels. Le pi-calcul, lui, fournit un outil pour représenter leurs interactions. Milner a montré en 1990 comment interpréter le lambda-calcul dans le pi-calcul. Plus précisément, il a montré comment interpréter deux stratégies d'évaluations du lambda-calcul, l'appel par nom et l'appel par valeurs. Se pose alors le problème de Full Abstraction: pour quelle notion d'équivalence de programme ces interprétations sont-elles correctes et complètes ? Si le problème a été résolu rapidement pour l'appel par nom, l'appel par valeur pose davantage de problèmes techniques...
Guarded recursion has emerged as a natural paradigm for programming with infinite data structures in type theory and high-assurance functional languages. In the first part of this talk, I will present some intuitions behind guarded recursion, using programming examples. In a second part, I will discuss ongoing work on a typed lambda-calculus equipped with rich facilities for defining and manipulating guarded recursive types.
An Asynchronous Soundness Theorem for Concurrent Separation Logic. Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. We develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems ⟦C⟧S and ⟦C⟧L which describe the operational behavior of the Code when confronted to its Environment (or Frame) – both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ⊢{P}C{Q} defines a winning and asynchronous strategy ⟦π⟧Sep with respect to both asynchronous semantics ⟦C⟧S and ⟦C⟧L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map ℒ:⟦C⟧S→⟦C⟧L, from the stateful semantics ⟦C⟧S to the stateless semantics ⟦C⟧L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races. This is joint work with Paul-André Melliès. Organization of the talk: In a first part, I will give a high level view of our semantics and of the soundness theorem, essentially as it appeared in our previous paper. In a second part, I will talk in more details about our new semantics of CSL, which has a more algebraic flavor (work in progress).
Realizability and parametricity are two well-known approaches to the semantics of System F, the architectural language for polymorphism. Many well-known realizability semantics can be recast in a simple topological form as induced by closure operators over sets of lambda-terms. This allows to generalize some completeness results known in the literature to a wide class of semantics (including Krivine's saturated sets and several variants of Girard's reducibility candidates), and to relate realizability with parametricity and dinaturality, an approach to parametricity arising from the functorial semantics of polymorphism. Our main result is that for a general class of realizability semantics (those which satisfy a particular topological property) one can prove a parametricity theorem'' stating that closed realizers are parametric and adinaturality theorem'' stating that closed realizers of positive types are dinatural. We compare our results with Wadler's approach which sees realizability and parametricity as some sort of adjoint functors. Finally, we briefly discuss the case of Girard's original definition of reducibility candidates, whose ``not trivial and somehow mysterious'' [Riba 2007] structure does not fit yet within our approach.
Finding lower bounds in complexity theory has proven to be an extremely difficult task. We analyze three proofs of lower bounds that use heavy techniques from algebraic geometry through the lense of dynamical systems. Interpreting programs as graphings – generalizations of dynamical systems that model Girard's Geometry of Interaction, we show that the three proofs share the same structure and use algebraic geometry to give a bound on the topological entropy of the system representing the program. This work, joint with Thomas Seiller, aims at proposing Geometry of Interaction derived methods to study dynamical properties of models of computation beyond Curry-Howard.
In this talk, I present a framework for recursive proofs of coinductive predicates, which are defined via functor liftings to fibrations. This framework is based on the so-called later modality and Löb-induction. Intuitively, the role of the later modality is thereby to control the use of coinduction hypotheses. Since the framework works on certain fibrations, it can be instantiated in very diverse situation like, for instance, set-based predicates and relations, quantitative predicates and relations, syntactic first-order logic, or dependent type theory. Apart from showing the underlying technical constructions of the framework, I will demonstrate how it can be used in those examples. Moreover, I will briefly talk about some recent progress, in collaboration with Katya Komendantskaya and Yue Li, in the direction of automatic proof search for this framework.
Je commencerai par une introduction basique aux différents outils utilisés dans mon domaine de recherche, à savoir la théorie des catégories, l'algèbre homotopique à la Quillen et l'interprétation de la logique à la Lawvere. Aucune connaissance n'est prérequise et je m'appuierai sur des analogies algébriques accessibles à tous mathématiciens (monoides, groupes, etc.) et sur des exemples pertinents en regard des thématiques du LIMD. Une fois ces notions introduites, je présenterai le résultat central de travaux récents effectués avec Paul-André Melliès : étant donnée une bifibration E-->B où la base et les fibres sont équipées de structures de catégories de modèles, quelles sont les conditions pour recoller ces dernières en une structure de catégorie de modèles sur la catégorie totale E ? J'essaierai enfin d'expliquer les motivations de ces travaux qui trouvent leur origine à la fois dans la théorie de l'homotopie catégorique et dans la sémantique de la théorie des types dépendents.
Structural operational semantics is a family of syntactic formats for specifying the operational semantics of programming languages, in the form of a labelled transition system. Fiore and his collaborators have proposed an abstract framework for structural operational semantics based on bialgebras, in which they managed to prove that bisimilarity is a congruence. However, their framework does not scale well to languages with variable binding. We give an abstract account of structural operational semantics based on Weber's parametric right adjoint monads, which encompasses variable binding. On the example of pi-calculus, the key idea is that, while Fiore models the syntax through a monad on a certain presheaf category, we use a subtly different presheaf category inspired by our previous work on sheaf models for concurrent languages. The crucial consequence is that the relevant monad is a parametric right adjoint. This yields a very simple proof of congruence of bisimilarity.
The ring of multivariate polynomials F[x_1, x_2, ..., x_n] is a unique factorization domain. We consider the following problem: ``Is there an 'efficient' algorithm that outputs a non-trivial factor of the given input polynomial''. This question has applications in algebraic complexity, for example, in proving the connection between polynomial identity testing (PIT) and lower bounds. In this talk, we will consider the closure of various classes of polynomial families under factorization. [Kaltofen86-90] studied this problem for VP. A slew of work in the recent years has brought it back into the limelight: [DSY09] studied circuits of small depth and factors of a special form, [Oliveria16] studied formulas of small depth, [DSS18] studied ABPs and formulas, [CKS18] studied the polynomial class VNP. We will take a look at these algorithms and state some open problems in the area.
La réécriture de dimension supérieure a pour origine des travaux de Squier sur le problème du mot dans les monoïdes. A partir d'une présentation d'un monoïde, Squier a pu calculer en basse dimension des invariants homotopiques de ce monoïde. Depuis, elle a été adaptée à d'autres structures, et en particulier aux PRO, où elle permet de prouver des théorèmes de cohérence comme celui de MacLane pour les catégories monoïdales. Par ailleurs, dans le cas des monoïdes, les constructions de réécriture ont été étendues en dimension supérieure. Au cours de cet exposé, je montrerai comment il est possible d'unifier ces théories de réécriture dans diverses structures. En particulier, ceci permet de réinterpréter les constructions effectuées en réécriture en termes homotopiques. Cette réinterprétation s'appuie en particulier sur la notion de omega-catégorie cubique et sur le produit de Gray.