The Croap Project

Design and Implementation of Programming Tools

Programmers and designers of programming formalisms or specifications face an increasingly complex task. This project aims to design and implement better adapted and more reliable programming tools. The Centaur system is the current embodiment of this research. The Centaur system is a formal tool to model and implement all aspects of programming languages. From the specifications of the syntax and the semantics of a given language, one can automatically produce a syntactic editor and interactive semantic tools (type checkers, interpreters) for this language. Semantic specifications are in an operational, or axiomatic, style, using the Natural Semantics approach. The Typol formalism (our computer version of Natural Semantics in the Centaur system), based on a logical framework, is highly declarative and expressive. Our study of programming paradigms leads us to formally produce from specifications interactive environments which are specially suit to a variety of programming languages. Thus we study tools for the ML language (functional programming), the Eiffel language (object-oriented programming), the SISAL language (parallel data-flow programming), and C (imperative programming). More recently, we also applied our techniques to Eiffel// (a parallel extension of Eiffel) and Java.

Research themes

Semantics of programming languages
Formal properties of programming languages
Mechanical proof of mathematic results
Construction of the Centaur interactive programming system

A few projects related to HPC

Selected Publications

A Formal Definition of the Dynamic Semantics of the Eiffel Language
Australian Computer Science Conference (ACSC), Brisbane, February 1993.
A Formal Semantics and an Interactive Environment for Sisal
Published in A. Zaky & T. Lewis editors, ``Tools and Environments for Parallel and Distributed Systems'' Kluwer Academic Publishers, ISBN 0-7923-9675-8, February 1996 .
A Formal Semantics for Sisal Arrays
Proceedings of Joint Conference on Information Sciences (JCIS'95), North Carolina, October 1995.
An Operational Semantics for the Eiffel// Language
INRIA Research Report no. 2732, November 1995.
Optimizing Sisal Programs: a formal approach
Euro-Par'96, International Conference on Parallel Processing, Springer-Verlag, LNCS 1123-1124, Lyon , August 1996.
A Natural Semantics for Eiffel Dynamic Binding
ACM Transactions on Programming Languages and Systems (TOPLAS), 18 (5) , November 1996.
Semantic-based visualization for parallel object-oriented programming
OOPSLA'96 (Object-Oriented Programming: Systems, Languages, and Applications), ACM Press, Sigplan Notices, Vol. 31, No. 10, San Jose, CA , October 1996.

Scientific leader

: Yves BERTOT; +33 4 93 65 77 39; Yves.Bertot@inria.fr; CROAP server

Isabelle Attali

Last modified: Thu Oct 16 11:17:29 MET DST