Unification is a central operation in the construction of a range of computational logic systems based on first-order and higher-order logics. First-order unification has a number of properties that dominates the way it is incorporated within such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respected the basic laws governing λ-binding (the equalities of α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been popular in various implemented systems and in various theoretical consideration, it is too weak for a number of applications. In this paper, we define an extension of pattern unification that is motivated by some existing applications and which satisfies these three properties. The main idea behind this extension is that the arguments to a higher-order, free variables can be more than just distinct bound variables: they can also be terms constructed from (sufficient numbers of) such variables using term constructor and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.
Thomas Streicher has reformulated Krivine's notion of classical realizability into abstract Krivine structures and showed that from any such structure one can build a tripos out of it. They are called Krivine triposes and form a subclass of relative realizability triposes in the sense of van Oosten and Hofstra. In this talk, I will present a characterization of those Krivine triposes, indeed, they are exactly boolean subtriposes of relative realizability triposes. I will also talk about a concrete construction of non-localic Krivine triposes. These results are from my master thesis supervised by Jaap van Oosten.
At POPL'96, Hughes, Pareto and Sabry presented an approach to the termination of closed ML-like programs based on type-checking and the abstract interpretation of a semantic notion of size. This approach was then extended by several authors to open terms and more complex type systems. In the first part, I will show how it can be extended in other directions: arbitrary user-defined notions of size and rewriting-based function definitions. In the second part, I will show how the decidability of type-checking (with size-induced subtyping) can be reduced to the existence, in the size algebra, of a smallest solution for any solvable set of inequalities, and show it for the successor algebra (which is enough to subsume Coq termination checker for instance).
In this talk I will present some recent work, with H. Michalewski, on the study of an extension of MSO on infinite trees with the so-called ``measure quantifier''. This kind of research is motivated, as I will discuss, by a long-standing open problem in the field of verification of probabilistic programs. I will state a negative (i.e., undecidability) result but also present some interesting (currently) open problems.
We introduce location graphs, a process calculus framework for modeling dynamic component systems. A key aspect of the framework is its ability to model different forms of component composition, dynamic component structures with sharing, and different forms of separation and encapsulation constraints. We present the operational semantics of the framework and hint at a type system for location graphs.
Directed algebraic topology is a young subject which takes inspiration from homotopy theory and concurrent processes. Differently from algebraic topology, it studies situations in which paths are, in general, not invertible. For this reason directed algebraic topology is particularly suitable for modelling non-reversible phenomena like concurrent processes, where processes do not reverse. In this talk, based on [1], I start from concurrent processes and show how directed algebraic topology is a natural model for it. [1] Martin Raussen, ``Contributions to Directed Algebraic Topology: with inspirations from concurrency theory'', Doctoral Thesis, Department of Mathematical Sciences, Aalborg University.
Les terrains de jeux sont des catégories double avec de la structure et des propriétés supplémentaires. Les quelques exemples de terrains de jeux connus s'appuient sur des constructions similaires. Je vais présenter une généralisation de cette construction de catégories double à partir de données plus simples que l'on appellera ``signature''. Moyennant certaines hypothèses sur la signature, on parvient à montrer une propriété cruciale des terrains de jeux : la propriété de fibration. On appliquera cette construction pour construire un terrain de jeux pour les jeux Hyland-Ong, et on comparera la structure obtenue aux structures classiques dans ces jeux.
Dans les calculs de processus (ccs, pi-calcul), les bisimulations modulos (up-to) sont des techniques de preuves utilisées pour montrer des équivalences entre processus [1]. Une méthode alternative, mais très similaire, consiste à montrer que deux processus sont solutions d'une même équation [2]. On présentera une telle technique reposant sur la non-divergence d'une solution minimale de l'équation, basée sur [3], qui illustre la correspondance entre bisimulations modulos et unicité des solutions, ainsi que les propriétés attendues d'un contexte dans un cadre abstrait (LTS). [1] Sangiorgi, Davide, and David Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge university press, 2003. [2] Sangiorgi, Davide. Equations, contractions, and unique solutions.'' POPL 2015. [3] Roscoe, A. W.Topology, computer science, and the mathematics of convergence.'' Topology and category theory in computer science. Oxford University Press, Inc., 1991.
Monotonicity is a fundamental notion in mathematics and computation. For usual real-valued functions R → R this simply corresponds to the notion that a function is increasing (or decreasing) in its argument, however this can be parametrised by any partially ordered domain and codomain we wish. In computation we deal with programs that compute Boolean functions, {0,1} → {0,1}. Restricting to increasing functions over this structure can be seen as prohibiting the use of negation in a program; for instance monotone Boolean functions are computed by Boolean circuits without NOT gates. The idea of restricting negation scales to other models of computation, and for some important classes of functions the formulation is naturally robust, not depending on the particular model at hand, e.g. for the polynomial-time functions. Monotone computational problems abound in practice, e.g. sorting a string and detecting cliques in graphs, and 'nonuniform' monotone models of computation, such as monotone circuits, have been fundamental objects of study in computational complexity for decades.
In this talk I will propose a project that develops logical characterisations of monotone complexity classes, via a proof theoretic approach. Namely, the project will identify theories of arithmetic whose formally representable functions coincide with certain monotone classes, and also develop fundamental recursion-theoretic programming languages in which to extract the monotone functions themselves. In particular the project focusses on the role of structural proof theory, i.e. the duplication and erasure of formulae, in controlling monotonicity.
À venir
A Theorem of Gao, Jackson and Seward, originally conjectured to be false by Glasner and Uspenskij, asserts that every countable group admits a strongly aperiodic subshift over a 2-symbol alphabet. Their proof consists of a quite technical construction. We give a shorter proof of their result by using the asymetrical version of Lovasz Local Lemma which allows us also to prove that this subshift is effectively closed (with an oracle to the word problem of the group) in the case of a finitely generated group. This is about joint work with Nathalie Aubrun and Stéphan Thomassé.
Travail en collaboration avec Arkady Leiderman, Ben Gurion University, Beer-Sheva, Israel. Un espace topologique $L$ est un espace ordonnable lorsqu'il existe un ordre total $leq$ sur $L$ tel que la topologie sur $L$ est engendrée par les intervalles ouverts (non nécessairement bornés) à extrémités dans $L$ (exemples: $N$, $Z$, $Q$, $R$; contre-exemple: $C$). Un espace $L$ est un espace héréditairement ordonnable si toute image continue de $L$ est ordonnable. On montre le résultat suivant: Si $L$ est un espace héréditairement ordonnable alors $L$ est un espace dénombrable et compact (i.e. un sous-espace compact de $R$, qui est donc homéomorphe a un ordinal dénombrable ayant un plus grand élément). En fait on montre un résultat plus général.
Bisimulation is used in concurrency theory as a proof method for establishing behavioural equivalence of processes. Up-to techniques are a means of enhancing this proof method. In this talk I will argue that up-to techniques can be of general use, and discuss how this is supported by our coalgebraic framework of up-to techniques, that provides enhanced proof techniques for a wide variety of systems and a wide variety of properties. I will discuss our recent work on extending this framework to cover equivalences for systems that involve silent transitions.
Le traitement catégorique de la théorie des probabilités formulé par Giry et Lawvere, basé sur la monade de probabilité G, permet de manipuler de façon élégante des probabilités d'ordre supérieur. Dans ce cadre, je présenterai une reconstruction du processus de Dirichlet, un objet largement utilisé en inférence bayésienne. Ce processus prend la forme d'une famille de mesures dans GG(X) indexée par M(X), où X est un espace Polonais et M(X) est l'espace des mesures finies non-zéro sur X. Sa construction repose sur deux outils dont l’intérêt dépasse le simple cas de la construction de Dirichlet. Le premier de ces outils est une version fonctorielle du théorème d'extension de Bochner adapté au cadre Polonais, qui permet d'étendre une famille projective de probabilités en une probabilité limite. Le second outil est une méthode de ``décomposition'' qui associe à tout espace Polonais zéro-dimensionnel une famille projective d'espaces finis, dont la limite projective est une compactification de l'espace originel. La combinaison de ces deux outils avec des propriétés bien connues de Dirichlet sur les espaces finis nous permet de reconstruire Dirichlet comme une transformation naturelle de M vers GG. Cette construction améliore les précédentes en ce qu'elle prouve la continuité de Dirichlet en ses paramètres.
PML est un langage de programmation en appel par valeurs similaire à ML, avec une syntaxe à la Curry (c'est à dire, pas de types dans les termes) et basé sur une logique d'ordre supérieur classique. Les termes apparaissent dans les types via un prédicat d'appartenance t ∈ A et un opérateur de restriction A | t ≡ u. La sémantique de ces deux constructeurs de types utilise une relation d'équivalence (observationnelle) sur les programmes (non typés). L'opérateur de restriction est utile pour l'écriture de spécifications tandis que l'appartenance permet d'encoder les types dépendants. La présence de l'équivalence nous permet également de relâcher la « value restriction » pour obtenir un type produit dépendant compatible avec la logique classique (ce qui n'avait pas été fait avant).
Le ``size-change principle'' (SCP) est un algorithme simple donnant un test partiel de terminaison qui s'adapte très bien aux langages fonctionnels où les fonctions sont définies de manière récursive par pattern-matching. En présence de constructeurs paresseux, le SCP donne également un test (partiel) de productivité : c'est sur ce principe que les tests (terminaison + productivité) de PML et Agda reposent. Malheureusement, en présence de type coinductifs, certaines définitions récursives bien typées terminent (i.e. sont productives) mais sont incorrectes et rendent Agda/PML inconsistants. En utilisant les travaux de L. Santocanale sur les preuves circulaires et les jeux de parité, je montrerais comment utiliser le SCP pour implanter un test partiel de totalité des définitions récursives qui généralise le test de terminaison/productivité, et garantie qu'une définition est correcte vis à vis de son type.
Le travail à présenter est une contribution à la spécification et la vérification des Systèmes à Base de Composants (SBC) modélisés avec le langage SysML. Les SBC sont largement utilisés dans le domaine industriel et ils sont construits en assemblant différents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coût de développement. Malgré le succès de l’utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en œuvre d’approches plus rigoureuses. Dans ce contexte, nous allons traiter principalement deux problématiques: La première est liée à la difficulté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle est la suivante : comment spécifier une architecture SBC qui satisfait toutes les exigences du système ? Nous proposons une approche de vérification formelle incrémentale basée sur des modèles SysML et des automates d’interface pour guider, par les exigences, le concepteur SBC afin de définir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le Model Checker SPIN et la LTL pour spécifier et vérifier les exigences. La deuxième problématique traitée concerne le développement par raffinement d’un SBC modélisé uniquement par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu’une composition d’un ensemble de composants élémentaires et réutilisables raffine une spécification abstraite d’un SBC. Dans cette contribution, nous exploitons les outils : Ptolemy pour la vérification de la compatibilité des composants assemblés, et l’outil MIO pour la vérification du raffinement.
The M2Disco (Multiresolution, Discrete and Combinatorial Models) research team aims at proposing new combinatorial, discrete and multiresolution models to analyse and manage various types of data such as images, 3D volumes and 3D meshes, represented as Digital Sur- faces (ie subset of Zn). One of their project called PALSE foam requires the computation of the shortest path between two points on a manifold. We are proposing the study of two algorithm for computing such a dis- tance, but also providing metric embedding inside a Discrete Exterior Calculus structure (DEC). We performs various tests regarding the two algorithms, but also con rm through experience DEC's operators con- vergence using suitable metric. This work is the base of both a research project named CoMeDiC (Convergent Metrics for Digital Calculus) and Ph.D. project.
Il existe de très nombreuses façons de représenter et discrétiser une courbe ou une surface, en raison notamment des applications envisagées et des modes d'acquisitions des données (nuages de points, approximations volumiques, triangulations...). Le but de cet exposé sera de présenter un cadre commun pour l'approximation des surfaces, dans l'esprit de la théorie géométrique de la mesure, à travers la notion de varifold discret. Ce cadre nous a notamment permis de dégager une notion de courbure moyenne discrète (à une échelle donnée) unifiée dont on présentera les propriétés de convergence et qu'on illustrera numériquement sur des nuages de points.