JFLA 2015 : exposés courts

Abstract: In this short paper, we report on the progress of the
implementation of the functional programming language CDuce with
polymorphic types. We highlight the challenges (theoretical and
implementation wise) of having an ml-style programming language with
parametric polymorphism and semantic subtyping. We also describe how
to compile a program using values from CDuce and OCaml, as well as the
issues encountered in the process. This ongoing work also raises
several language design questions, that we think are of interest to
(or maybe have been answered by) the community at large.

Abstract: KaSim is a stochastic simulator, written in OCaml, for rule-based models described in the Kappa Language. The simulator implements an algorithmically efficient rule-based version of the Gillespie technique for generating sample paths that follow proper stochastic chemical kinetics. The simulator employs a so-called network-free technique in which rules are applied by pattern matching to a (very) large graph that represents the contents of a system at a given time. The algorithm does not identify molecular species, i.e. n complexes (molecular species) of the same kind are represented as n isomorphic graph components. Such a graph is still much (at times infinitely) smaller than an explicit representation of the implied reaction network. The trade-off, however, is a time-consuming update scheme after each event. This can become burdensome in certain cases.
We aim to design a new implementation of the Kappa simulator that will benefit as much as possible from the merits of both an explicit reaction network and a network-free approach at the same time. We propose to discuss various algorithmic issues with the JFLA community.

Abstract: Dedukti is a proof checker based on rewriting and dependent types. It
implements the λΠ-calculus modulo, a very expressive logical framework in-
troduced by Cousineau and Dowek.
This talk will introduce Dedukti through a series of examples showing how
rewrite rules can be conveniently used to write programs in a dependently typed
framework. We will also present efficient encodings of different logics into the
λΠ-calculus modulo and show how to check theorems in these logics with De-
dukti.

Abstract: L'avènement des systèmes à ressources restreintes dans notre quotidien exige des garanties sur leur fonctionnement. Parmi celles-ci, la consommation mémoire est un des éléments essentiels. Il est intéressant d'utiliser des mécanismes d'allocation et de récupération dynamique de mémoire pour une utilisation optimale de celle-ci. Mais cette dynamicité rend difficile la prévision de la quantité maximale de mémoire nécessaire au bon fonctionnement d'un programme. Pour permettre cette prévision, on propose le développement conjoint d'un langage à la ML muni d'un mécanisme de régions et d'une analyse fournissant une borne supérieure de la quantité de mémoire consommée. Cette analyse exploite les annotations de régions pour tenir compte de la mémoire libérée à travers celles-ci et ainsi affiner la borne supérieure de son occupation Comme le style de programmation influence les dépendances entre régions, il impacte aussi le résultat de l'analyse. Au final, on parvient à fournir une borne supérieure pour des programmes fonctionnels et impératifs manipulant des structures linéaires et arborescentes.

Abstract: Le développement de Patoline (un nouveau système de composition de documents) nécessite un parseur extensible d'OCaml sans contrainte, notamment sur l'analyse lexicale. Nous présentons ici un environnement de développement léger pour l'analyse syntaxique, conçu en deux mois pendant l'été 2014 pour répondre à ce besoin.

Le système propose une syntaxe intuitive de type BNF, sans récursion à gauche. Les parseurs sont traduits vers des expressions OCaml utilisant DeCaP, notre bibliothèque de combinateurs monadiques, et sont donc des expressions de première classe.

Pour optimiser les combinateurs, nous utilisons des continuations et une méthode de prédiction des premiers caractères acceptés par une grammaire. Sur la grammaire d'OCaml, on obtient en moyenne une analyse cinq fois plus lente qu'avec le parseur d'origine et deux fois plus rapide qu'avec Camlp4. De plus, on dispose de combinateurs inspirés de la notion de continuation délimitée pour optimiser les grammaires. Notons que nous gérons aussi les grammaires ambigües.

Les extensions de la syntaxe d'OCaml utilisent un mécanisme de quotation et d'anti-quotation similaire à celui de Camlp4, avec un peu plus de simplicité et moins de contraintes.

Abstract: Finite vector spaces are vector spaces of finite dimensions, over
a finite field. The category of finite vector spaces and linear
functions is known to form a model of linear logic. In this
extended abstract, we discuss its properties when used as a model
of simply-typed lambda-calculi.

This extended abstract summarizes arXiv:1406.1310 which should
have been presented at ICTAC'14.

Note: the abstract consists of 3 pages ; the last 2 pages only contain the bibliography.

Abstract: TrustInSoft est une jeune entreprise qui promeut l'utilisation des
méthodes formelles dans l'industrie en proposant des analyseurs de
code source construits au dessus de la plateforme libre Frama-C.

Suite à des problèmes de performance avec l'interface graphique de Frama-C,
TrustInSoft s'est lancée dans le développement d'une nouvelle interface
utilisant les technologies du Web dans le but de résoudre ces
problèmes.

Grâce au compilateur Js_of_ocaml, le développement d'une telle interface est simplifié pour des programmes en OCaml et possède de nombreux avantages
par rapport à l'utilisation d'une bibliothèque comme GTK+.

Abstract: De nombreux langages de programmation utilisent une valeur spéciale pour représenter un résultat indéterminé ou la valeur d'une variable non initialisée. Afin d'éviter les erreurs classiques résultant de confusion entre cette valeur (nommée {\tt NULL}, {\tt nil}, {\tt None}) et une valeur définie, certains langages (Hack, Swift, pour citer deux langages de conception industrielle récente) utilisent le typage pour indiquer la présence possible d'une valeur indéfinie (que nous nommerons {\tt NULL} dans cet article). Un tel type, contenant {\tt NULL}, est appelé {\em nullable}. {\em A contrario}, un type non nullable ne peut pas contenir {\tt NULL}: ses valeurs peuvent donc être utilisés librement pour des opérations classiques (arithmétique pour des valeurs numérique, dé-référencement pour des pointeurs, ou encore appel pour des valeurs fonctionnelles).

Nous présentons dans cet article un algorithme d'inférence de types pour un langage statiquement typé, d'ordre supérieur, doté de types nullables. Nous présentons d'abord deux techniques, la première étant fondée sur un système de types très simple, et la seconde utilisant un encodage à base des variants polymorphes du langage OCaml. Nous montrons les faiblesses de ces deux approches et introduisons un algorithme d'inférence, fondé sur la collection et la résolution de contraintes de sous-typage, qui ne présente pas les faiblesses des deux systèmes précédents. Cette inférence a été prouvée correcte et nous donnons ici le schéma de cette preuve.

Abstract: L'isolation mémoire est une propriété fondamentale pour garantir la sécurité
des systèmes exécutant plusieurs processus de différents niveaux de
sensibilité au dessus d'un noyau de confiance s'exécutant avec le plus haut
niveau de privilège (noyau monolithique, micro-noyau, hyperviseurs, etc.). En
effet, afin de garantir la confidentialité et l'intégrité du noyau et des
processus, il est nécessaire d'interdire les accès illégaux (c.-à-d. ne
répondant pas à la politique de sécurité attendue du système) en lecture et en
écriture des processus vers d'une part la mémoire des autres processus et
d'autre part vers la mémoire du noyau. Dans cet article nous présentons une
formalisation en Coq d'un système d'exploitation simplifié. Il comprend un
ordonnanceur préemptif et un gestionnaire mémoire utilisé par le noyau et par
les processus pour allouer dynamiquement des pages en s'appuyant sur une unité
matérielle de gestion mémoire (MMU). La modélisation proposée utilise une
logique de Hoare définie au dessus d'une monade d'état. Le travail exposé
propose une définition de l'isolation entre les processus et produit la preuve
d'isolation sur le système formalisé.

Abstract: Operations manipulating algebraic data types – structures, variants – and arrays are frequently concerned only with a limited subset of their input. However, specifications and proofs concerning unaffected parts have to be manually explicited which can be a cumbersome task.
In order to simplify the proof burden, we have developed a prototype of a dependency analysis, working on an abstraction of a strongly-typed, functional language. Its role is to delimit the input fragment on which the output depends. It is a flow-sensitive, context-sensitive, intraprocedural analysis that makes use of interprocedural approximations. Our analysis considers arrays, structures and variants. For the latter, it simultaneously computes a subset of possible constructors.
Generally, our analysis targets complex transition systems and is meant to contribute towards a solution for automated invariant preservation inference. In particular, we are applying it on a high-level model of an operating system. Our long-term goal is to combine the dependency analysis with an effects analysis, meant to detect relations between inputs and outputs.

Abstract: Ceci est un résumé de l'article:

Kento Emoto, Frédéric Loulergue, and Julien Tesson, ``A Verified
Generate-Test-Aggregate Coq Library for Parallel Programs
Extraction'', In {\em Interactive Theorem Proving (ITP)}, LNCS 8558, pages
258-274, Springer, 2014.