Je pense traiter trois themes :
(1) un resume du projet MRG (Mobile Resource Guarantees) ou en d'autres termes pourquoi
l'extraction de bornes est connectee au code mobile.
(2) un survol des differents approches a la caracterisation de
classes de complexite dans le cadre d'un langage fonctionnel
du premier ordre : Cobham / Bellantoni-Cook / Leivant-Marion /
Jones/ Hofmann
(3) des nouvelles idees sur comment inferer qu'une fonction
n'augmente pas sa taille (non-size increasing).
We consider the issue of using type systems to check that functional programs
have a polynomial time complexity. We examine in this perspective the use of light
affine logic as a type system for lambda-calculus. We discuss type inference and show its
decidability by reducing typability to the solving of systems of inequations on words.
Nous présentons CDuce, un langage fonctionnel d'ordre supérieur, avec typage statique et dispath dynamique à l'execution. CDuce est un langage généraliste, mais adapté à la manipulation de documents XML, l'objectif étant de pouvoir exprimer des manipulation complexes directement dans CDuce. D'un point de vue théorique, le système de type s'appuie sur une sémantique ensembliste des types, qui permet de définir de manière naturelle une relation de sous-typage, et des combinaisons booléennes de types.
CDuce possède une puissante opération de filtrage (pattern-matching) qui permet d'exprimer (sous forme d'expressions regulières, ou à la main avec des motifs récursifs) des opérations complexes d'extraction. Là encore, la sémantique ensembliste du filtrage permet de déduire des algorithmes de typage très précis, ainsi que des schémas de compilation efficaces.
We describe a new class of tree automata, and a related logic on trees, with applications to the processing of XML documents and schemata.
XML documents, and several other forms of semi-structured data, may be roughly described as edge labeled trees. Therefore it is natural to use tree automata to reason on them and try to apply the classical connection between automata, logic and query languages. This approach has been followed by various researchers and has given some notable results, especially when dealing with Document Type Definition (DTD), the simplest standard for defining XML documents validity. But additional work is needed to take into account XML Schema, a more advanced standard, for which regular tree automata are not satisfactory. A major reason for this inadequacy is the presence of an associative-commutative operator in XML Schema, the ``all group'', and the inherent limitations of regular tree automata in dealing with associative-commutative algebras.
The class of automata considered here, called Sheaves Automata, is a tailored version of automata for unranked trees with both associative and associative-commutative symbols already proposed by the authors. In order to handle both ordered and unordered operators, we combine the transition relation of regular tree automaton with regular word expression and counting constraints. This extension appears quite natural since, when no counting constraints occurs, we obtain Hedge Automata, a simple yet effective model for XML schemata, and when no constraints occur, we obtain regular tree automata.
Building on the classical connection between logic and automata, we also present a decidable tree logic, specifically designed for XML-like documents, which could be used as a foundation for a query language.
A dependent type system distinguishing different running modes in a higher-order communication language is given; some security policies can be enforced based on this typing in a migration-independent model.
We present a typed calculus for manipulating semistructured data that contains hidden information. The data model is simple labeled trees with a hiding operator. Data manipulation is based on pattern matching, with types that track the use of hidden labels.
The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data.
We study some basic questions concerning the descriptive and discriminating power of AL, focusing on the equivalence on processes induced by the logic (=L). We consider MA, and two Turing complete subsets of it, MAIF and MAIFsyn, respectively defined by imposing a semantic and a syntactic constraint on process prefixes.
The main contributions include: coinductive and inductive operational characterisations of =L; an axiomatisation of =L on MAIFsyn; the construction of characteristic formulas for the processes in MAIF with respect to =L; the decidability of =L on MAIF and on MAIFsyn, and its undecidability on MA.
Cet exposé présentera la conception de Lucid Synchrone, un langage synchrone dédié à la programmation de systèmes réactifs. Le langage combine le synchronisme de Lustre et des traits présents dans les langages fonctionnels de la famille ML (e.g, polymorphisme, ordre supérieur). Ce langage a été obtenu en plongeant Lustre dans un cadre fonctionnel et en géneralisant les techniques connues pour celui-ci. En particulier seront abordés le lien entre calcul d'horloge et typage; le développement d'analyses statiques rejetant les programmes non productifs ou l'utilisation des techniques venant des co-algèbres pour obtenir une compilation efficace vers du code séquentiel. L'exposé se terminera par une discussion des développements en cours et les diverses extensions envisagées.
Boxed Ambients were introduced as a variant of Mobile Ambients, with the purpose to better formalize concepts like read/write access and mandatory security policy in a distribute scenario. In this work, we study information flow security in NBA, with the aim of developing a sound type system that provides static guarantees of absence of unwanted flow of information for well typed processes. With respect to other works in the process algebras framework, we introduce a new definition of non interference and we discuss peculiar source of unwanted information flow in distributed calculi.