Search

Partial Evaluation in Prolog (generally associated to Folding/Unfolding techniques) is a code optimization technique, which transforms a readable and structured program in a more efficient program (that is to say better adapted to the interpreter or compiler). These programs are Prolog programs semantically equivalent with respect to the least Herbrand model. Our context is the operational equivalence of programs, and not the efficiency of program transformations.

Unfoldings of oriented graphs generate infinite trees that we generalize by weighting arrows of these graphs. Indexes along a branch are added during unfoldings and the result indexes variables. We study formal properties of these graphs (substitution, equivalence, unification, ...). We use them to solve the halting problem of a recursive head-rewriting rule (as in PROLOG-like languages).

National audience; Les architectures neuromorphiques sont l’une des approches les plus prometteuses pour continuer l’amélioration des capacités de calcul après la fin imminente de la loi de Moore. En effet les réseaux de neurones affichent aujourd’hui des succès retentissants dans le domaine de l’intelligence artificielle et sont naturellement tolérants à la variabilité du matériel due aux processus de fabrication aux échelles nanométriques. Ils permettent en outre d’espérer un fonctionnement très économe en énergie. Nous présentons ici une étude de cas montrant la flexibilité de notre simulateur en logiciel libre d’architectures neuromorphiques, N2S3, et les gains énergétiques potentiels de ces architectures.

International audience; Model Driven Architecture (MDA) design approach proposes to separate design into two stages: implementation independent stage then an implementation-dependent one. This improves the reusability, the reusability, the standability, the maintainability, etc. Here we show how MDA can be augmented using a formal refinement approach: B method. Doing so enables to gradually refine the development from the abstract specification to the executing implementation; furthermore it permits to prove the coherence between components in low levels even if they are implemented in different technologies.