Inria Awards 2011

Grand Prize to Gérard Huet

Grand Prize to Gérard Huet Inria / C. Tourniaire

By awarding the Grand Prize to Gérard Huet, Inria honours an exemplary achievement and scientific career. As a pioneer in the French school of thought in terms of information technology, Gérard Huet has had a profound influence on many sectors of IT science.

Gérard Huet discovered information technology during his studies at Supaéro which, at the time, was one of the few establishments offering a small computing centre. ‘I was able to learn about programming and I liked it straight away. I simultaneously signed up for a master’s in IT and did a summer internship at the CEA which had the biggest machines existing in France at the end of the sixties.’ He left for the United States to do his thesis in Artificial Intelligence (AI), a field that was very much in vogue in those days. But he was disappointed by a discipline that he found quite unconvincing and chose to direct his work towards automatic demonstration which he saw as a more exacting science.

On his return to France, he began working at IRIA in 1972 joining the team led by Maurice Nivat. With other young researchers just back from the United States, such as Gilles Kahn and Jean Vuillemin, he formed the community called ‘Bat8’ in Building (Bâtiment) 8 of the Rocquencourt site. Sharing the same culture and the same conviction that it was necessary to establish the mathematical bases of IT to ensure its development, together they would contribute to the emergence of a French school of thought in terms of information technology fundamentals in the 1980s. This community forged lasting and productive ties with various European partners such as the University of Edinburg and Chalmers University in Göteborg. In this context, Gérard Huet explored various subjects, from automatic demonstration to rewriting and type theory, with the methodological rigour that characterises all his work.

The themes that occupied the first thirty years of my career all aimed to mechanize mathematics in order to ensure the certification of software demanding a high degree of security and reliability, such as those used in air transport and network protocols or to verify very complex mathematical theorems.

We can cite major contributions in three domains. Firstly his work in the field of logic and type theory with the unification algorithm for typed lambda calculus, known as the Huet algorithm, which earned him the 1998 Herbrand Award. Then there is his work on functional programming especially that conducted with Jean-Jacques Lévy on sequential calculus. In parallel to this, his team perfected the Caml language, then its successor Objective Caml, a reliable and efficient programming language. Lastly we should mention his work on the logic and mechanization of mathematics through the Calculus of Constructions, alongside Thierry Coquand and Christine Paulin-Möhring. It was upon these bases that the Coq proof assistant was developed. ‘Teamwork is very important in such projects’, insists Gérard Huet, ‘because it helps you to keep up a long term effort combining fundamental works leading to publication with durable software creations applicable at actual size. I would like to pay tribute to the work of many colleagues and students in this framework ».

The zipper, a software engineering innovation resulting from a fundamental data structure invented by G. Huet in the 1990s The zipper, a software engineering innovation resulting from a fundamental data structure invented by G. Huet in the 1990s

Having himself spontaneously followed the path of thematic mobility, he advises his students to change subject every 10 years to get a wider outlook. After spending 3 years in charge of international relations for Inria during which he built up a team at the service of science and created the Internship program, he radically changed tack to concentrate on computational linguistics which combines his interest in languages and his love of Indian culture. He brought a new perspective and resolved the problem of segmentation into words of sentences in Sanskrit. He developed a system of analysing Sanskrit, part of which he published in the Zen computational linguistics library in 2005 and, with his student Benoît Razet, perfects a relational programming methodology based on a generalisation of finite machines (Eilenberg machines). «It is a perfect example of the virtuous approach which consists in going from applications to theory. Once we have defined the solution for a particular application, we generalise it in the appropriate manner. This allows us to obtain general methods, but above all pertinent ones.»

Gérard Huet attaches the same scientific value to his software work as he does to his articles. «For me, writing a program is like writing literature. The program’s source code must be sufficiently clear and aesthetic to be well understood and easily updated. For example, my lesson on lambda calculus is the explanation of a library of executable programs, enabling students to learn by using these algorithms». An example that is not taken by chance since, for this highly reputed scientist, teaching is a noble activity that a researcher owes it to himself to perform. It is a way of testing new and still vague ideas and to discover new questions. But «it also has an important social function because there are more and more very technical tertiary professions in society today», adds Gérard Huet. «Training for managers, engineers, teachers, and so on, is of a higher level.»

When asked about his vision of information technology of the future, he insists upon the need to «keep glancing backwards.». «After having seen at first hand the development of this science from the outset, I can say that, despite being aware of the countless possibilities offered by IT, we were constantly surprised: we never imagined 30 years ago that one day everyone would have a computer, just as 10 years ago we never imagined the development of social networks.»Therefore it is more about being tactical than prospective, being opinionated enough to embark upon a long voyage but also knowing how to ride the waves that form and to leave them when they start to run out of momentum. An approach crowned by his entrance into the French Academy of Sciences in 2002 and his nomination as Doctor Honoris Causa by Chalmers University in Göteborg in 2004. He has also received the prestigious EATCS Award from the European Association for Theoretical Computer Science in 2009. And what about the Inria Grand Prize? «It is a great honour to be the first to receive this prize.»

Testimonies

Benoit RAZET, who did his thesis on computational linguistics with Gérard Huet and is currently working at Bucknell University in the United States

Benoit Razet

« Gérard Huet really takes an interest in all his students including those preparing a thesis. He is a very good teacher with heaps of energy and he is also an atypical character. I remember his executable lecture notes on lambda calculus which allowed us to experiment with the algorithms and therefore gave a very practical side to a subject that is otherwise very theoretical. He is also a very available and helpful thesis director, who knows how to share his vision of the areas of specialisation that he has covered to resolve a new problem. He encouraged me to present my work in public, to write publications, to go abroad. I really appreciate what he did for me! »

Jean-Marie HULLOT, former CTO of Apple

Jean-Marie Hullot

« Gérard Huet is known for being extremely thorough in his work. He is a master of formal algebra. When faced with a practical problem he knows how to take a step back to find the level of abstraction that will allow him to resolve it. This approach enables him to successfully tackle very diverse problems ranging from type theory to the analysis of Sanskrit. It is with him that I got a taste for programming as a complementary part of theory, before devoting most of my career to the industry. »

Sylvie BURINI, former assistant of the ‘Formel’ project directed by Gérard Huet

Sylvie Burini

« Underneath the very serious and slightly distant manner that put me very much in awe of him when I first began working with him, he is a very warm person who knows how to share his enthusiasm, for travelling for example. He also has a lot of humour and is quite a quirky character with a predilection, in the 80s, for all things red, from the Austin which for a long time transported him to Rocquencourt to the big square and red glasses that he sometimes wore! In connection with work, he is demanding but always takes the time to clearly explain what he expects. »

Amba KULKARNI, Head of Department of Sanskrit Studies, University of Hyderabad and Indian coordinator of the associate team Sanskrit

Amba Kulkarni

« Gerard Huet is a leading computer scientist and a Sanskrit computational linguist. There is still no parallel for his efficient Sanskrit segmentiser. He looks at the Sanskrit Grammar purely from a computer scientist's viewpoint. I am amazed by the innovativeness in his implementations such as his enhancement of FST leading to a segmentiser and his introduction of phantom phonemes to handle anomalous behaviour of consonants. Working with Gerard Huet is always a fun and a learning experience, be it a theoretical discussion on Panini or planning a symposium or porting of a system. »

Christine PAULIN-MOHRING, PROVAL team, Inria Research Centre in Saclay - Île-de-France

Christine Paulin-Mohring © INRIA / Photo Jim Wallace

« I prepared my thesis with Gérard Huet at the end of the 1980s, at the beginning of the calculus of constructions which is the basis of the Coq proof assistant. Everything was to be done with limited means of calculation. It was a risky wager and its success is due to Gérard’s vision and tenacity with regard to the "right" solutions to implement, such as using the Caml language. One of his principles which has influenced his students is that a result should not only be demonstrated but should also be programmed. »

Keywords: Gerard Huet Inria Awards Grand Prize