Gérard Berry’s Home Page
|
INRIA – Project Indes 2004, route des Lucioles 06902 Sophia Antipolis, France Tel. +33 4 92 38 76 41 Assistant tel. +33 4 92 38 77 92
(Anais Cassino) Mail: gerard.berry@sophia.inria.fr Photographs: http://pbase.com/gberry |
Ingénieur général des mines, detached to INRIA Sophia
Antipolis.
Professor at Collège de France, 2009-2010
Professor at Collège de France, 2007-2008
Member, Académie des sciences, Académie des technologies and Academia Europaea
President
of the INRIA Evaluation Committee
Delegate of the inter-section of applications at Académie des sciences
Déformaticien au Collège de ‘Pataphysique (Pour les publications en ‘Pataphysique, voir section 4 en fin de page)
Les transparents sont ici au format pps, et préservent donc toutes les animations. Ils sont lisibles sous PowerPoint, OpenOffice, et d’autres lecteurs gratuits téléchargeables sur le Web
Leçon inaugurale du 19/11/2009 : Penser, modéliser et maîtriser le calcul
Cours 1 du 25/11/2009 : Syntaxe, sémantique, calculabilité :
Cours 2 du 02/12/2009 : Le lambda-calcul : réductions, causalité et déterminisme
Cours 3 du 09/12/2009 : Sémantiques, information et points fixes
Cours 4 du 16/12/2009 : Automates et systèmes de transitions
Cours 5 du 06/01/20010 : Parallélisme asynchrone
Cours 6 du 13/01/20010 : Parallélisme synchrone et vibratoire
Cours 8 du 13/01/20010 : La nécessaire mais délicate coopération de modèles + Les questions
CV Summary
1. Scientific and Industrial
Activities
1.1. Recursive programs,
lambda-calculus, and sequentiality
1.2. Automata, real-time, and
Esterel
1.3. Circuit synthesis,
causality, and verification
1.4. Industrial development of
Esterel
1.5. Courses at Collège de France
3.3. Journal and Book Articles
4. Publications ‘Pataphysiques
My global research
revolves around five fields: mathematical models of computation, associated
programming and circuit description languages, implementation of compilers to
hardware and software, usage of formal verification systems, and industrial
applications.
My initial work
(1973-1976) at Ecole des Mines de Paris and IRIA was about understanding how to
revert the order of recursive computations, for instance by transforming the
Fibonnacci iterative algorithm into the iterative one. I proved the optimality
in time and space of Rice’s algorithms to compute the Ackerman function as
defined by its classical program. In this study, I introduced the notion of a
stable function that became fundamental for what followed.
With Jean-Jacques Lévy,
I then studied minimal and optimal syntactic computations in recursive programs
and in the l-calculus. After that, I switched to the full
abstraction problem specified by Plotkin and Milner: build a semantical model
of PCF (typed l-calculus + arithmetic)
that exactly contains all functions that are definable by syntactic terms. I
first established the syntactic properties of stability and sequentiality of
the l-calculus, which
essentially show that it cannot express parallel computation. I developed the
stable model, which preserves stability in the semantics, unlike the classical
Scott Model.
In 1977, I moved to the
new Ecole des Mines site at Sophia-Antipolis. With Pierre-Louis Curien, I
developed the sequential algorithm model, where functions are replaced by
algorithms that can be presented in two ways: pairs of a stable function and a
computation strategy, or programs in a simple kernel programming language. We showed that this model forms a cartesian
closed category, hence an non-functional model of the l-calculus. With M. Devin and F. Montagnac, we then
developed the CDS programming language. The study of categories as models of
the lambda-calculus was also at the root of the categorical abstract machine
(CAM) which started the development of CAML.
In
1982, INRIA opened its new site in Sophia-Antipolis, and I created a joint
project between Ecole des Mines and INRIA with Gérard Boudol. At that time, I
switched to automata theory and real-time programming. With Jean-Paul Rigault
and Jean-Paul Marmorat, we gave the initial definition of the new Esterel
synchronous programming language dedicated to embedded systems. In cooperation
with the Lustre teams of Nicolas
Halbwachs and Paul Caspi and the Signal team of Albert Benveniste and Paul Le
Guernic, we studied the associated synchronous model of concurrency. I
essentially focused the theoretical study on the definition and usage of
deterministic preemption structures in this model. With Laurent Cosserat, we
developed the fisrt Esterel v1 compiler, soon followed by the Esterel v2
compiler developed with Philippe Couronné. Esterel v2 was based on the
adpatation of a fast and beautiful algorithm developed by Ravi Sethi (then at
Bell Labs) and myself to translate regular expressions into automata. We
conducted industrial experiments at Bertin and Dassault Aviation, where we
started a fruitful and longstanding cooperation with Emmanuel Ledinot.
In
1986, we started the development of a much more efficient compiler called
Esterel v3, based on decisive fundamental research results by Georges Gonthier.
This compiler was then industrialized by the companies Cisi Ingéniérie and ILOG
and used by several customers.
In
1990, I joined Jean Vuillemin’s group at Digital Equipment as a part-time
consultant. The group was developing the Perle FPGA-based machine and using it
as a fast co-processor of alpha-based workstations. It was pretty clear how to
develop data-flow hardware designs, but much less clear how to develop complex
control-intensive designs. EstereI seemed to be a good language to specify
them. I created a new translation from Esterel to circuits, which was readily
implemented in the new Esterel v4 compiler. This new approach also had a decisive
impact on software applications of Esterel: generating a circuit simulator in C
instead of an explicit finite state machine made it possible to scale up to any
application size, completely avoiding the potential exponential code size
blow-up of Esterel v3. It also lead to major progress in understanding
causality issues in Esterel and relating them to constructive logic. With Tom
Shiple, we could show that a combinational cyclic circuit is electrically
stable for all delays if and only if its Boolean equations can always be solved
by using only constructive propositional logic, i.e., by disallowing usage of
the excluded middle law X or not X = true.
This lead to a new Esterel v5 compiler, soon followed by a modular version
Esterel v6.
In
1999, I started cooperating with Michael Kishinevsky at Intel on extensions of
Esterel to be able to define any kind of for-real synchronous circuits. This
required the definition of deep extensions of the language to be able to
support arbitrary data path and bit manipulation structures. We defined the new
Esterel v7 language and studied how to compile it. The language is
characterized by a smart arithmetic and bitvector type-checker that
automatically ensures optimal sizing of intermediate variables in data paths.
In
January 2001, I joined the Esterel Technologies company created the year
before, as its Chief Scientist. I directed the implementation of the Esterel v7
compiler (with A. Boulan, L. Arditi, M. Buchholtz, M. Perreaut, B. Pagano, and
others). We solved many fundamental and technical problems needed for
production usage: extending the language to support multiclock design;
supporting a ECO-enabled flow (ECOs are late patches necessary when it has
become too expensive to recompile, re-place and re-route the circuit); ensuring
safe translation to VHDL and Verilog that are not well defined languages;
linking the compiler with the Esterel Studio graphical interface and with the
Prover SL formal verification system; instertion of the tools in complete
industrial flows, etc. The Esterel Studio complete design and verification
environment is used in production by ST Micro and Texas Instruments and in
research by Intel, Philips (now NxP), ST Microelectronics, and Texas
Instruments. It has also been widely distributed in Esterel Technologies’
academic program.
In
2003, Esterel Technologies acquired SCADE, the leading tool for synchronous
avionics development, based on the Lustre Technology developed in Verimag,
Grenoble, and used by major avionics companies such as Airbus. I participated
in the development of the SCADE language and environment, and, in particular,
of the new Scade 6 language that integrates the best of Lustre and Esterel. See
www.esterel-technologies.com for more information.
In
2009-2010, I have been selected again by Collège de France to occupy the first
year of the new chair Informatique et
sciences numériques (Computer Science
and Digital Sciences). I will teach a course called Penser, modéliser et maîtriser le calcul informatique (Thinking about, modeling, and mastering computation), where I will discuss why and how
to model automatic computation, from the original sequential models to the
current models of parallel computation.
In
2007-2008, I have been selected by Collège de France to occupy the yearly
Technology Innovation Chair Liliane Bettencourt, sponsored by the
Bettencourt-Schueller Foundation. I decided to give a general audience computer
science course called « Pourquoi et comment le monde
devient numérique » (Why and How the World Becomes
Digital). The inaugural lecture analyzed why the digitization idea and the
fantastic expansion of computers changed the world, and how this change will
continue. It also explains the scientific background of this revolution. The
inaugural lecture was followed by 7 2-hour course / seminar sessions,
respectively on algorithms, circuits, programming languages, embedded systems,
program verification, networks, images, cryptography, and a conclusion. For each subject, I invited experts from
research and industry to give the seminars. The inaugural lecture and all
courses and seminars (except cryptography) are available as videos (in French).
The inaugural lecture is also available as a book in French.
Since March 2009, I am
a member of the Indes INRIA project, which is dedicated to diffuse programming,
i.e., the global programming of the set of computerized objects we now have at
our disposal: computers, telephones, TVs, domestic appliances, etc. Safe
programming of this network of devices will require tight cooperation between
many sequential and parallel programming models. My own work is about
understanding which models are needed where and how to make the models
cooperate.
2009-2010 : Professeur
at Collège de France, Chaire informatique et sciences numériques
2009 / 2010
Course: Penser, modéliser et
maîtriser le calcul (Thinking about, modeling, and mastering computation).
Videos and slides of the lectures and seminars (in French) will be available
here.
2009- :
Director of Research at INRIA Sophia Antipolis.
2008 : Professeur at Collège de France, Chaire d'Innovation
technologique 2007 / 2008
Course: Pourquoi et comment le monde
devient numérique (Why and How the World Becomes Digital). Videos and
slides of the lectures and seminars (in French) are available
here.
2001-2009
: Chief Scientist of Esterel Technologies.
1990-2001
: Regular consultant at Digital Equipment, Schneider Electric, Synopsys,
Cadence Design Systems, and Intel.
1977-2001 : Director of Research at Ecole des Mines de Paris, Sophia Antipolis
site. Co-head of a joint project with INRIA Sophia Antipolis.
1979 : Docteur d’état in Mathematics at Université Paris
VII, option Computer Science.
1970-1977 :
Researcher at Ecole des Mines de Paris, Paris site.
1970 : Entered Corps National des Ingénieurs des Mines.
1967 : Entered Ecole Polytechnique.
2008 : Chevalier de l'Ordre du mérite.
2005 : Great Prize of the EADS Foundation for
applications of sciences to industry.
2005
: Member, Académie des technologies
2002
: Member, Académie des sciences.
2001 : Nominee, World Technology Awards.
1999 : Science and Defense award.
1994 : Chevalier
de l'Ordre des palmes académiques.
1993 : Member, Academia
Europaea
1990 : Monpetit Prize of Académie des sciences.
1979 : Bronze medal of C.N.R.S.
Invited
speaker in 34 international conferences :
Bits&Chips
2007 (Eindhoven), FMICS'2007 (Berlin), Ada Europe 2007 (Geneva), FDL'2006 (Darmstadt),
CSR'2006 (St Petersburg), TACAS'2005 (Edinburgh), VLSI'2004 (Mumbai),
ICCAD'2003 (San Jose), HLDVT'2002 (Cannes), SAME'2001 (Sophia Antipolis),
CHARME'2001 (Edinburgh), FEMSYS'2001 (Munich), FST&TCS'2000 (New Delhi),
ASE'2000 (Grenoble), CHARME'99 (Bad Herrenalb), CONCUR'98 (NICE), POPL'98 (San
Diego), DSL'97 (Santa Barbara), CAV'97 (Haifa), CHDL'97 (Toledo), TACAS'97
(Twente), AMAST'96 (Munich), ICSC'95, (Bangkok), IWLS'95 (Lake Tahoe), MFPS'94
(Manhattan, Kansas), LICS'94 (Paris), POPL'94 (Portland), FSTTCS'93 (Bombay),
REX'93 (Amsterdam), CONPAR'92 (Lyon), ESEC'91 (Milano), TAPSOFT'90 (Brighton),
IFIP'89 (San Francisco), STACS'86 (Paris).
Invited speaker at the first Milner Lecture,
Edimburgh Université, 1996.
Invited speaker at the Kieburtz Symposium, 2003
(OGI Portland, USA).
Invited speaker for the Tata Consultancy
Services Distinguished Lecture, 2006 (Pune, India).
Keynote speaker for the IBM Programming
Languages Day, 2006 (Yorktownheigths, USA).
Invited
speaker at several summer schools : Marktoberdorf 1992 et 2008, Laser
2007, several schools in India, Malaisia, Thailand, etc.
Penser, modéliser et maîtriser le calcul
G. Berry, Fayard, Collection Collège de France, Nov. 2009.
Pourquoi et comment le monde devient numérique
G. Berry, Fayard,
Collection Collège de France, Jan. 2008.
D. Potop, S. Edwards,
and G. Berry. Springer, 2007.
The Constructive Semantics of Esterel
G. Berry. Draft book,
current version 3.0, Dec. 16th, 2002.
The Esterel Language Primer, version v5_91
G. Berry. Current version
Esterel v5_91, june 2000.
Modèles complètement adéquats et stables des
lambda-calculs typés
G.Berry. Thèse de Doctorat d'Etat, Université Paris VII (1979).
Calculs
Ascendants des Programmes Récursifs.
G.Berry. Thèse de Troisième Cycle,
Université Paris VII, 1976.
Pourquoi
et comment le monde devient numérique, résumé des cours.
G. Berry. In Cours et travaux du Collège de France,
année 2007-2008. Collège
de France, 2008.
Esterel: a Formal
Method Applied to Avionic Software Development
G. Berry, A. Bouali, X.
Fornari, E. Ledinot, E. Nassor, R. de Simone. Science of Computer Programming
36(2000) 5-25.
An Implementation of
Constructive Synchronous Constructive Programs in Polis
G. Berry, E. Sentovich.
Formal Methods in Systems Design 17(2), October 2000, Kluwer Academic Publisher.
G. Berry. Proof,
Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C.
Stirling and M. Tofte, editors, MIT Press, Foundations of ComputingSeries,
2000.
A Hardware Implementation of Pure Esterel
G. Berry. Sadhana,
Academy Proceedings in Engineering Sciences, Indian Academy of Sciences, vol. 17,
part 1 (1992) 95-130.
Esterel on Hardware
G. Berry. Philosophical
Transactions Royal Society of London A, vol. 339 (1992) 87-104.
The Synchronous
Programming Language ESTEREL: Design, Semantics, Implementation
G. Berry and G.
Gonthier. Sience of Computer Programming, vol. 19, no. 2 (1993) 87-152.
G. Berry and G. Boudol.
Theoretical Computer Science, vol. 96 (1992) 217-248.
Incremental development
of an HDLC entity in Esterel
G. Berry and G.
Gonthier. Comp. Networks and ISDN Systems 22, (1991) 35-49.
The Synchronous
Approach to Reactive and Real-Time Systems
A. Benveniste and G.
Berry. Proceedings of the IEEE, vol. 79, no. 9 (1991) 1270-1282.
From Regular
Expressions to Deterministic Automata
G. Berry and R. Sethi.
Theoretical Computer Science 48 (1986) 117-126.
Theory and Practice of
Sequential Algorithms: the Kernel of the Programming Language CDS
G. Berry and P-L.
Curien. in Algebraic Methods in Semantics, Cambridge University Press (1985)
35-88.
Full Abstraction for
Sequential Languages: the State of the Art
G. Berry, P-L. Curien
and J-J. Lévy. in Algebraic Methods in Semantics, Cambridge University Press
(1985) 89-132.
Sequential Algorithms
on Concrete Data Structures
G. Berry and P-L.
Curien. Theoretical Computer Science, vol. 20 (1982) 265-321.
Minimal and Optimal
Computations of Recursive Programs
G. Berry and J-J. Lévy. Journal of ACM, vol. 26, no. 1 (1979) 148-175.
Bottom-up Computations
of Recursive Programs
G. Berry, RAIRO
Informatique théorique, vol. 10, n. 3
(1976).
SCADE: Synchronous design and validation of
embedded control software
G. Berry. Proc. General
Motors India Lab Workshop, Bangalore, 2007, Springer-Verlag Lecture Note, 2007.
L. Arditi, G. Berry, M.
Kishinevsky, and M. Perreaut. Proc. Designing Correct Circuits DCC'06, Vienna,
Austria.
Late Design Changes (ECOs) for Sequentially
Optimized Esterel Designs
L. Arditi, G. Berry,
and M. Kishinevsky. Proc. Formal Methods in Computer Aided Design (FMCAD'04),
Austin, Texas, USA.
System Level Design and Verification using a
Synchronous Language.
G. Berry, M. Kishinevsky,
S. Singh. Proc. ICCAD'03, San Jose.
Toplevel Validation of System on Chip.
G. Berry, A. Bouali, J. Dormoy, L. Blanc. Proc. HLDVT'2001,
Cannes.
G. Berry, E. Sentovich.
Proc. CHARME'2001, Edinburgh, Correct Hardware Design and Verification Methods,
Springer-Verlag LNCS 2144.
Efficient Latch
Optimization Using Incompatible Sets
E. Sentovich, H. Toma,
and G. Berry. International Digital Automation Conference DAC'97, Anaheim,
1997.
Latch Optimization in Circuits Generated from
High-Level Descriptions
H. Toma, E. Sentovich,
and G. Berry. Proc. International Conf. on Computer-Aided Design ICCAD'96.
Constructive Analysis of Cyclic Circuits
T. Shiple, G. Berry,
and H. Touati. Proc. International Design and Testing Conference IDTC'96,
Paris, France (1996).
Preemption in Concurrent Systems
G.Berry. Proc.
FSTTCS'93, Springer-Verlag Lecture Notes in Computer Science 761 (1993) 72-93.
Communicating Reactive Processes
G. Berry, S. Ramesh,
and R. K. Shyamasundar. Proc. 20th ACM Conf. on Principles of Programming Languages
(POPL), Charleston, Virginia (1993).
Optimized Controller Synthesis Using Esterel
G. Berry and H. Touati.
Proc. Intl. Workshop on Logic Synthesis, Lake Tahoe, USA (1993).
Real Time Programming:
Special Purpose or General Purpose Languages
G. Berry. Information
Processing 89, G.X. Ritter (Ed.), Elsevier Science Publishers B.V.,
North-Holland (1989) 11-18.
The Synchronous
Programming Language ESTEREL and its Mathematical Semantics
G. Berry and L.
Cosserat. In Seminar on Concurrency, Springer-Verlag LNCS 197 (1984) 389-448.
ESTEREL: Towards a
Synchronous and Semantically Sound High-Level Language for Real-Time
Applications
G. Berry, S. Moisan,
and J-P. Rigault. Proc. IEEE Real-Time Systems Symposium, Arlington, Virginia,
IEEE Catalog 83CH1941-4 (1983) 30-40.
Programming with
Concrete Data Structures and Sequential Algorithms
G. Berry. Proc. ACM
Conf. on Functional Programming Languages and Computer Architecture, Wentworth-by-the-sea,
USA (1981).
On the Definition of
Lambda-calculus Models
G. Berry. Proc. Int.
Coll. on Formalization of Programming Concepts, Peniscola, Spain, Lecture Notes
in Computer Science 107, Springer-Verlag (1981) 218-230.
A Survey of Some Syntactic
Results in the Lambda-calculus
G. Berry and J-J. Lévy.
Proc. Ann. Conf. on Mathematical Foundations of Computer Science, Olomouc,
Tchecoslovaquia, Lecture Notes in Computer Science 74, Springer-Verlag (1979).
Stable Models of Typed
Lambda-calculi
G. Berry. Proc. 5th
Coll. on Automata, Languages and Programming(ICALP), Lectures Notes in Computer
Science 62, Springer-Verlag (1978) 72-89.
Séquentialité de l'évaluation formelle des
Lambda-expressions
G. Berry. In Program Transformations, 3eme Colloque International sur la
Programmation, DUNOD, Paris, B. Robinet ed. (1978) 67-80.
Program Equivalence and
Canonical Forms in Stable Discrete Interpretations
G. Berry and B.
Courcelle. Proc 3rd Coll. on Automata, Languages and Programming (ICALP),
Edinburgh University Press (1976).
Manifeste
pour la réhabilitation du pavillon des poids et mesures
G. Berry, Viridis Candela, Correspondancier du
Collège de ‘Pataphysique, no 1, pages 33-60 (2007)
Les
Shadoks sont-ils décervelables ?
G. Berry, Viridis Candela, Le Correspondancier du
Collège de ‘Pataphysique, no 7, pages 57-70 (2009)
Un mauvais Cardeur
G. Berry, Viridis Candela, Le Correspondancier du
Collège de ‘Pataphysique, no 8, pages 51-52 (2009)