Nous presentons un encodage simple et direct de la machine abstraite de Krivine (KAM) dans le calcul de processus d'ordre superieur HOcore, en utilisant un nombre tres restreint de canaux de communication. Cet encodage montre qu'il est possible de capturer l'expressivite du lambda-calcul en HOcore des que l'on fixe l'ordre d'evaluation. Nous donnons egalement une nouvelle borne inferieure pour le nombre minimal de restrictions necessaire pour rendre l'equivalence de programmes dans HOcore indecidable.
Les langages flot de donnees synchrones a la Lustre proposent un formalisme equationnel de haut niveau dedie a la conception et l'implantation de systemes temps reel. Ils sont traditionnellement restreints aux systemes critiques ne necessitant pas de calcul intensif ; en particulier, le code imperatif genere ne contient pas naturellement de boucles. Lucy-n est une variante recente de Lustre plus adaptee aux traitements multimedias. Dans cet article, nous proposons une extension de la semantique de Lucy-n ou les flots transportent des rafales de valeurs plutot que de simples scalaires, ainsi qu'un systeme de types qui caracterise la taille de ces rafales. L'ambition est d'adapter les techniques de generation de code usuelles pour produire des boucles imbriquees.
Dans cet article nous etendons le lambda-calcul bi-chrome presente aux JFLA 2012 pour y introduire la polychromie. On definit une nouvelle transformation, par beta-expansion, qui regroupe les expressions de meme couleur, chaque couleur pouvant representer une unite de calcul. On ne se contente plus de pouvoir expliciter la localite d'un calcul dans un modele a deux couleurs comme pour les clients-serveurs mais nous pouvons traiter les applications multi-tiers. Les proprietes de correction, de terminaison et de confluence de cette nouvelle transformation sont demontrees a l'aide de Coq.
The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verification in Coq of properties of programs manipulating the global state effect. These properties are expressed in a proof system which is close to the syntax, as in effect systems, in the sense that the state does not appear explicitly in the type of expressions which manipulate it. Rather, the state appears via decorations added to terms and to equations. In this system, proofs of programs thus present two aspects: properties can be verified {\em up to effects} or the effects can be taken into account. The design of our Coq library consequently reflects these two aspects: our framework is centered around the construction of two inductive and dependent types, one for terms up to effects and one for the manipulation of decorations.
Dans Frama-C , plate-forme d'analyse de code C developpee en OCaml, un journal est un script OCaml genere automatiquement et permettant de reproduire les actions utilisateurs, notamment e ectuees via l'interface utilisateur. Outre la reproductibilite des resultats qui est necessaire dans un contexte industriel soumis a des exigences de certi cation fortes comme la norme avionique DO-178C, un journal permet d'automatiser le pilotage de l'outil dans un contexte d'utilisation particulier. Cet article presente comment le mecanisme de generation du journal de Frama-C, appele journalisation et requerant intrinsequement de l'introspection, a ete developpe en OCaml, en combinant typage statique et dynamique.
We present a technique for deriving semantic program analyses from a natural semantics specification of the programming language. The technique is based on a particular kind of semantics called pretty-big-step semantics. We present a pretty-big-step semantics of a language with simple objects called O'While and specify a series of instrumentations of the semantics that explicitates the flows of values in a program. This leads to a semantics-based dependency analysis, at the core, e.g., of tainting analysis in software security. The formalization has been realized with the Coq proof assistant.
ReactiveML est un langage dedie a la programmation de systemes combinant des parties algorithmiques et reactives. Il s'agit d'une extension de ML avec des constructions pour la concurrence inspirees des langages synchrones. Celles-ci permettent d'obtenir une tres grande expressivite, mais leur implantation efficace represente un defi. Dans cet article, nous presentons l'implantation de ReactiveML, de la compilation a l'implantation du moteur d'execution en OCaml. Nous decrivons egalement une implantation parallele en memoire partagee du moteur d'execution utilisant le vol de tâches. L'approche choisie permet d'obtenir une execution efficace meme en presence de structures de controle complexes. Elle s'etend simplement au cas parallele avec des resultats experimentaux prometteurs.
This article describe a mechanism of well-typed communications able to abstract the underlying physical transport protocol MOTS-CLÉS : communication typé, migration de code, middleware
This article describes the library of projects embedded in Frama-C, which is an extensible platform dedicated to development of source-code analysis of C software. Through this presentation, we detail an original aspect of ML functors which uses their imperative and compositional parts. That is the only well-typed way to implement the required functionality. Furthermore we show a singular example of a hugely-applied functor. This article also introduces the Frama-C platform through one of its main features, the notion of project. MOTS-CLES : systeme de modules, foncteur, programmation imperative et fonctionnelle, genie logiciel, analyse statique.
While taking over an existing software written in OCaml, cleaning the code was necessary before further development. To this end, a tool to find elements used or not would be useful to save time. We present an analysis of OCaml code based on the construction of an annotated dependency graph. The vertices of this graph are the elements of the OCaml language (values, modules, types, . . . ) and the annotations on the edges specify the kind of dependency (use, inheritance, . . . ). Thereafter, a language to select elements of this graph is defined to find non-referenced elements (revealing potentially useless code), or other elements such as record fields never consulted. This analysis is implemented and available in free software Oug. Some statistical analysis on the annotated graph are discussed in an attempt to ease the understanding of the organization of the analyzed code. MOTS-CLES : OCaml, dependances, fouille au code, statistiques, code inutile, code mort
Modern multi-core machines are conceived to efficiently execute explicitly parallel assembly programs. Current technology is moving away from instruction-level parallelism, exploitable without changes in the software, toward task-level parallelism requiring modifications in programs. In this context exploiting parallelism entails either exploiting new parallelizing toolchains, or programming in new (higher-level) languages supporting explicit parallelism. In other words exploiting multi-core machines may follow two different routes: changing the programming model or hiding from the user the complexity of this task by delegating to a compiler the parallelization of a higher-level program, preferably in a declarative style. In either case compiled programs must be efficient on such architectures, hence the efficiency of the language runtime support is also central. In particular, when the language is high-level and provides automatic memory management, the garbage collector risks to be the bottleneck limiting the overall performance gain. This paper is an experience report on the association of two softwares which we have implemented, an interpreter for a functional language augmented by a construct for asynchrone computations and a garbage collector for parallel machines. The two tools combined provide the user (be it a human or a compiler), a way to exploit the hardware parallelism of a shared-memory multi-processor machine with a declarative and essentially functional programming style. MOTS-CLES : multi-coeur, future, ramasse-miettes, programmation fonctionnelle
ion d’horloges dans les systèmes synchrones flot de données ∗ Louis Mandel & Florence Plateau LRI, Université Paris-Sud 11 INRIA Saclay {mandel,plateau}@lri.fr
