Nous abordons dans ce papier les preuves de terminaison de fonctions recursives par l'usage d'un ordre bien fonde. Nous proposons une utilisation de l'ordre sur les ordinaux : pour ce faire, nous donnons une representation des ordinaux de ω ω , posons une definition de leur relation d'ordre basee sur cette representation et en montrons la bonne fondation. Nous illustrons le pouvoir d'expression de cette approche sur quelques exemples de definitions de fonctions au schema de recursivite complexe. Leur terminaison est obtenue en definissant, pour chacune, un plongement des arguments dans un ordinal. L'avantage de cette approche est d'une part la facilite d'expression des fonctions denies par filtrage, et d'autre part son aspect systematique qui ouvre la perspective de l'usage d'une heuristique de decision pour la terminaison.

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.

Unmarshalling primitives in statically typed language require, in order to preserve type safety, to dynamically verify the compatibility between the incoming values and the statically expected type. In the context of programming languages based on parametric polymorphism and uniform data representation, we propose a relation of compatibility between (unmarshalled) memory graphs and types. It is defined as constraints over nodes of the memory graph. Then, we propose an algorithm to check the compatibility between a memory graph and a type. It is described as a constraint solver based on a rewriting system. We have shown that the proposed algorithm is sound and semi-complete in presence of algebraic data types, mutable data, polymorphic sharing, cycles, and functional values, however, in its general form, it may not terminate. We have implemented a prototype tailored for the OCaml compiler [17] that always terminates and still seems sufficiently complete in practice.

Cet article decrit comment donner une expression formelle du blason comme un langage de combinateurs afin d'etre a meme de produire son interpretation graphique : l'armoirie.

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE SUITE 6TM certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO-178B, IEC 61508, EN 50128 and such.

High-level tools have become unavoidable in industrial software development processes. Safety-critical embedded programs don't escape this trend. In the context of safety-critical embedded systems, the development processes follow strict guidelines and requirements. The development quality assurance applies as much to the final embedded code, as to the tools themselves. The French company Esterel Technologies decided in 2006 to base its new SCADE SUITE 6TM certifiable code generator on Objective Caml. This paper outlines how it has been challenging in the context of safety critical software development by the rigorous norms DO-178B, IEC 61508, EN 50128 and such.

Cet article relate une experimentation pedagogique dans laquelle nous avons concu un cederom pour accompagner un cours d'initiation a l'informatique. Ce cederom procure un environnement de developpement enrichi d'exercices et d'auto-evaluations. De facon autonome c'est-a-dire non connectes a Internet, les etudiants peuvent etudier leur cours, ecrire des programmes et les soumettre pour obtenir une appreciation immediate de leur travail. Les reponses sont accumulees puis transmises dans une base de donnees centrale ou elles peuvent etre analysees et assurer ainsi un suivi personnalise.

We describea teachingexperimentwherean introductorycourseto Computer Scienceis accompaniedby a computerizedtrainingengine.This wholeengine reliesontheexistenceof aninterpreterof thetaughtprogramminglanguagethat allows usto offer quizzesaswell asexerciseswith someautomaticmarkingfacility. Studentsmaythenperformtheir homework with animmediatefeedback withoutbeingconnectedto theInternet.However students’answersareeventually gatheredin a centraldatabasewherethey may beanalyzedthusproviding themeansfor “personalcoaching”. Demonstrationsof theenginewill bepresentedat theconference.

Polymorphic parametric languages, statically typed, `a laML, do not need to keep types inside their values duringruntime to have a safe execution. Nevertheless this typeinformation gives new possibilities for debugging, allowsto extend the language to manipulate types as values. Itcan be stored either in stack or in heap.To manage the additional type information, we proposein this paper to divide the heap in a value space and amirror space. The first space is used to store values, the...