Corrado Böhm
Pour les articles homonymes, voir Böhm.
| Naissance | |
|---|---|
| Décès | |
| Nationalité | |
| Formation | |
| Activité |
| A travaillé pour | |
|---|---|
| Membre de | |
| Directeurs de thèse | |
| Site web | |
| Distinctions |
Corrado Böhm, né le à Milan et mort le à Rome[2], est un informaticien théoricien italien.
Professeur émérite à l'université de Rome « La Sapienza », il est connu principalement pour ses contributions à la théorie de la programmation structurée, aux mathématiques constructives, à la logique combinatoire, au lambda-calcul, à la sémantique et à l'implémentation des langages de programmation fonctionnelle.
Biographie
[modifier | modifier le code]Corrado Böhm fait ses études en Suisse à partir de 1942. Il obtient un diplôme d'ingénieur en électro-technique en 1946 à l'École polytechnique fédérale de Lausanne (qui s'appelait alors encore École polytechnique de l'Université de Lausanne (EPUL)) et devient ensuite chercheur à l'ETH Zürich, où il commence à s'orienter vers l’informatique à l'occasion de l’arrivée de la machine Zuse Z4 de Konrad Zuse qui est installée à l'ETH en 1950. Il obtient un doctorat en mathématiques en 1952[3]sous la direction d'Eduard Stiefel et de Paul Bernays (qui lui fait connaître les machines de Turing) avec une thèse intitulée Calculatrices digitales du déchiffrage de formules logico-mathématiques par la machine même dans la conception du programme[1], publiée ensuite sous un titre légèrement différent[4]. Il y décrit un compilateur complet, qui plus est méta-circulaire (en), c'est-à-dire qui utilise des mécanismes de traduction d'un langage de programmation écrits dans ce même langage[5].
En 1951, Böhm retourne en Italie. Il travaille d'abord chez Olivetti, puis à partir de 1953 à l'Istituto per le Applicazioni del Calcolo (it) du Consiglio Nazionale delle Ricerche à Rome (dirigé alors par Mauro Picone auquel il va succéder). Le premier ordinateur italien moderne (FINAC) y est installé en coopération avec l'entreprise Ferranti de Manchester. Böhm est responsable de son exploitation, puis devient responsable de la programmation d'applications en analyse.
Dans les années 1960, Böhm commence à enseigner dans les universités de Rome et de Pise, et s'oriente vers l'informatique théorique. Il démontre avec Giuseppe Jacopini, alors son étudiant, le structured program theorem (en), aussi appelé « théorème de Böhm-Jacopini »[6] qui est un des articles pionniers de la programmation structurée (ou « programmation sans Goto » d'après Edsger W. Dijkstra). Le théorème affirme que l'on peut formuler les algorithmes en utilisant comme structures de contrôle uniquement la mise en séquence d'instructions, les tests de branchement dirigés par l’évaluation d'une expression booléenne ou l'itération d'une partie de programme à l'intérieur d'une boucle.
Dans les années 1960 également, Böhm développe ses recherches sur le Lambda-calcul d'Alonzo Church et sur la programmation fonctionnelle. En 1968, il démontre un théorème important[7], selon lequel deux expressions du lambda-calcul qui ont des formes normales différentes pour la β-conversion et la η-conversion ne peuvent être identiques. Avec Wolf Gross, Böhm élabore un langage de programmation fonctionnelle basé sur le lambda-calcul et sur la logique combinatoire de Haskell Curry. Ils proposent la machine abstraite CUCH comme modèle d'implantation de ce langage.
Avec Alessandro Berarducci, Böhm établit un isomorphisme entre les types de données algébriques strictement positives et les lambda-termes polymorphes, connu depuis comme le codage de Böhm-Berarducci[8].
En 1968 il est nommé professeur titulaire à Modène, puis à l'université de Turin, où il crée le département d'informatique qui, au début, était composé d'un seul bureau et d'une IBM 360 utilisée aussi par les autres départements. À partir de 1974, Böhm est professeur à Rome, où il organise aussitôt une conférence internationale sur le lambda-calcul[9].
À partir de 1964, Böhm est membre, avec Dana Scott, Christopher Strachey et d'autres, du Working Group 2.2 de l'IFIP (Formal description of programming concepts). À partir de 1988 il est membre du IFIP Working Group Functional Programming.
Honneurs et prix
[modifier | modifier le code]- En 1994, Corrado Böhm est docteur honoris causa de l’université de Milan
- En 2001, il est récipiendaire du prix EATCS[10]
- Il est membre de l'Academia Europaea
Publications (sélection)
[modifier | modifier le code]- Corrado Böhm, « Calculatrices digitales. Du déchiffrage des formules mathématiques par la machine même dans la conception du programme », Annali di Mat. pura e applicata, série IV, t. XXXVII, , p. 1–51 (lire en ligne).
- (en) Corrado Böhm, « On a family of Turing machines and the related programming language », ICC Bulletin, vol. 3, , p. 185–194
- (en) Corrado Böhm et Guiseppe Jacopini, « Flow diagrams, Turing Machines and Languages with only Two Formation Rules », Comm. of the ACM, vol. 9, no 5, , p. 366–371 (DOI 10.1145/355592.365646).
- (it) Corrado Böhm, « Alcune proprietà delle forme β-η-normali nel λ-K-calcolo », Pubblicatione del Istituto per le Applicazioni del Calcolo, Rome, no 696, (lire en ligne).
- (en) Corrado Böhm et Mariangiola Dezani-Ciancaglini, « A CUCH-machine: The automatic treatment of bound variables », International Journal of Parallel Programming, vol. 1, no 2, , p. 171-191.
- (en) Corrado Böhm et Alessandro Berarducci, « Automatic Synthesis of typed Lambda-programs on Term Algebras », Theoretical Computer Science, vol. 39, , p. 135–154 (DOI 10.1016/0304-3975(85)90135-5).
- (en) Corrado Böhm, « Functional Programming and Combinatory algebras », dans M. P. Chytil, L. Janiga et V. Koubek (éditeurs), MFCS 1988, Carlsbad, Springer, coll. « Lecture Notes in Computer Science Vol. 324 », (DOI 10.1007/BFb0017128), p. 14-26.
- (en) Corrado Böhm, « Theoretical Computer Science and Software Science: The Past, the Present and the Future (Position Paper) », dans TAPSOFT, (DOI 10.1007/BFb0030582), p. 3-5.
Notes et références
[modifier | modifier le code]- (en) « Corrado Böhm », sur le site du Mathematics Genealogy Project
- (it) « È morto Corrado Böhm - Maurizio Codogno », Il Post, (lire en ligne, consulté le )
- « Corrado Böhm » dans le Mathematics Genealogy Project.
- Böhm 1954.
- Donald Knuth et Luis Trabb Pardo, « The early development of programming languages », dans Nicholas C. Metropolis, J. Howlett et Gian-Carlo Rota (éditeurs), A History of computing in the twentieth century : a collection of essays with introductory essay and indexes, New York, N.Y., Academic Press, (ISBN 9780124916500, OCLC 13434539), p. 197-273.
- Böhm et Jacopini 1966.
- Böhm 1968.
- Beyond Church encoding: Boehm-Berarducci isomorphism of algebraic data types and polymorphic lambda-terms sur le site okmij.org.
- Corrado Böhm (éditeur), I.e. Lambda-calculus and Computer Science Theory : Proceedings of the Symposium Held in Rome, March 25-27, 1975, Springer, coll. « Lecture Notes in Computer Science, Volume 37 », , 370 p. (ISBN 978-3-540-07416-8).
- Page du prix EATCS
Annexes
[modifier | modifier le code]Articles connexes
[modifier | modifier le code]- Liste d'informaticiens et précurseurs de l'informatique
- P′′ (en), un langage de programmation minimal
Liens externes
[modifier | modifier le code]- (en) « A Collection of Contributions in Honour of Corrado Böhm on the Occasion of his 70th Birthday », Theoretical Computer Science, vol. 121, no 1&2, (présentation en ligne)
- (it) Page personnelle de Corrado Böhm.
- (it) Corrado Böhm sur l'université de Rome.
- Ressources relatives à la recherche :
- Naissance en janvier 1923
- Naissance à Milan
- Étudiant de l'École polytechnique fédérale de Lausanne
- Étudiant de l'École polytechnique fédérale de Zurich
- Professeur à l'université de Rome « La Sapienza »
- Personnalité en informatique théorique
- Lauréat du prix EATCS
- Informaticien italien
- Décès à 94 ans
- Décès en octobre 2017
- Décès à Rome
- Docteur honoris causa de l'université de Milan