Corrado Böhm

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 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[2], publiée ensuite sous un titre légèrement différent[3]. 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[4].

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 (it) 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 »[5] 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[6], 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[7].

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[8].

À 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.

• En 1994, Corrado Böhm est docteur honoris causa de l’université de Milan
• En 2001, il est récipiendaire du prix EATCS[9]
• Il est membre de l'Academia Europaea

• 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,‎ 1954, 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,‎ juillet 1964, p. 185–194
  Introduit le langage P" (en), le premier langage impératif Turing-complet sans instruction GOTO.
• (en) Corrado Böhm et Guiseppe Jacopini, « Flow diagrams, Turing Machines and Languages with only Two Formation Rules », Comm. of the ACM, vol. 9, n^o 5,‎ 1966, 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, n^o 696,‎ 1968 (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, n^o 2,‎ 1972, p. 171-191.
• (en) Corrado Böhm et Alessandro Berarducci, « Automatic Synthesis of typed Lambda-programs on Term Algebras », Theoretical Computer Science, vol. 39,‎ 1985, 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 », 1988 (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, 1997 (DOI 10.1007/BFb0030582), p. 3-5.