Book contents
- Frontmatter
- Contents
- List of contributors
- Preface
- 1 Determinacy in a synchronous π-calculus
- 2 Classical coordination mechanisms in the chemical model
- 3 Sequential algorithms as bistable maps
- 4 The semantics of dataflow with firing
- 5 Kahn networks at the dawn of functional programming
- 6 A simple type-theoretic language: Mini-TT
- 7 Program semantics and infinite regular terms
- 8 Algorithms for equivalence and reduction to minimal form for a class of simple recursive equations
- 9 Generalized finite developments
- 10 Semantics of program representation graphs
- 11 From Centaur to the Meta-Environment: a tribute to a great meta-technologist
- 12 Towards a theory of document structure
- 13 Grammars as software libraries
- 14 The Leordo computation system
- 15 Theorem-proving support in programming language semantics
- 16 Nominal verification of algorithm W
- 17 A constructive denotational semantics for Kahn networks in Coq
- 18 Asclepios: a research project team at INRIA for the analysis and simulation of biomedical images
- 19 Proxy caching in split TCP: dynamics, stability and tail asymptotics
- 20 Two-by-two static, evolutionary, and dynamic games
- 21 Reversal strategies for adjoint algorithms
- 22 Reflections on INRIA and the role of Gilles Kahn
- 23 Can a systems biologist fix a Tamagotchi?
- 24 Computational science: a new frontier for computing
- 25 The descendants of Centaur: a personal view on Gilles Kahn's work
- 26 The tower of informatic models
- References
25 - The descendants of Centaur: a personal view on Gilles Kahn's work
Published online by Cambridge University Press: 06 August 2010
- Frontmatter
- Contents
- List of contributors
- Preface
- 1 Determinacy in a synchronous π-calculus
- 2 Classical coordination mechanisms in the chemical model
- 3 Sequential algorithms as bistable maps
- 4 The semantics of dataflow with firing
- 5 Kahn networks at the dawn of functional programming
- 6 A simple type-theoretic language: Mini-TT
- 7 Program semantics and infinite regular terms
- 8 Algorithms for equivalence and reduction to minimal form for a class of simple recursive equations
- 9 Generalized finite developments
- 10 Semantics of program representation graphs
- 11 From Centaur to the Meta-Environment: a tribute to a great meta-technologist
- 12 Towards a theory of document structure
- 13 Grammars as software libraries
- 14 The Leordo computation system
- 15 Theorem-proving support in programming language semantics
- 16 Nominal verification of algorithm W
- 17 A constructive denotational semantics for Kahn networks in Coq
- 18 Asclepios: a research project team at INRIA for the analysis and simulation of biomedical images
- 19 Proxy caching in split TCP: dynamics, stability and tail asymptotics
- 20 Two-by-two static, evolutionary, and dynamic games
- 21 Reversal strategies for adjoint algorithms
- 22 Reflections on INRIA and the role of Gilles Kahn
- 23 Can a systems biologist fix a Tamagotchi?
- 24 Computational science: a new frontier for computing
- 25 The descendants of Centaur: a personal view on Gilles Kahn's work
- 26 The tower of informatic models
- References
Summary
Abstract
This paper is an overview of 15 years of collaboration between R&D teams at Dassault Aviation and several research projects at INRIA. This collaboration was related to Gilles Kahn's work on generic programming environments, program transformation, and user interfaces for proof assistants.
It is also an evocation of personal memories about Gilles, my perception of the impact of the research he carried out and supervised, and his dedication to INRIA.
Introduction
Since 1990, Dassault Aviation has been working on some formal methods and programming tools developed at INRIA by Gilles' research group (CROAP) or by other groups led by scientists close to him such as Gérard Berry and Gérard Huet.
Formal methods, more specifically the synchronous languages Esterel and Lustre or the proof assistant Coq, have been evaluated and introduced in our engineering processes to enhance our development tools for safety critical software, especially software embedded in flight control systems.
As for the programming tools developed by CROAP with the generative environment Centaur, it happened that in 1995 some of its language-specific instantiations were targeting scientific computation. More precisely, they were designed to assist some classical transformations of large Fortran codes (ports, parallelization, differentiation). Since Dassault Aviation has always developed its computational fluid dynamics (CFD) codes in-house, there was some motivation in our company to experiment tools that claim to partially automate some time consuming tasks done manually at that time.
- Type
- Chapter
- Information
- From Semantics to Computer ScienceEssays in Honour of Gilles Kahn, pp. 547 - 560Publisher: Cambridge University PressPrint publication year: 2009