Corrado Böhm#

Corrado Böhm was born on January 17th 1923 in Milan, Italy, and lived there until 1942, when he left Italy for Switzerland. At the time he was a student in Engineering.

He graduated in Electrical Engineering in 1946, at the University of Lausanne, in Switzerland, and shortly afterwards he became a research assistant at the ETH (the Swiss Federal Institute of Technology) in Zürich. The beginning of Corrado’s activity in Computer Science can be traced back to 1947, when he was asked to collaborate in the performance evaluation of the computing machine Z4 of Konrad Zuse, the computer pioneer. The encounter with Zuse and his work was a crucial moment in the development of Corrado’s scientific ideas. His Ph.D. dissertation in Mathematics, which he submitted in 1951, was in fact a first bridge between the computer and the mathematics disciplines. In his thesis Corrado developed a language, a machine, and a translation method for compiling that language on the machine.

As remarked by D.E. Knuth in his paper “The early development of programming languages” (with L.T. Pardo, in: Metropolis, Howlett and Rota, eds., A History of Computing in the Twentieth Century, Annals of the History of Computing (Academic Press, New York, 1980) 197–268): “Böhm’s dissertation was especially remarkable because he not only described a complete compiler, he also defined that compiler in its own language! And the language was interesting in itself, because every statement (including input statements, output statements and control statements) was a special case of an assignment statement.” This is in fact the first known example of what is now called a meta-circular compiler. Corrado described his compiler four years before FORTRAN was defined and seven years before the definition of LISP! The dissertation was published as (3). His official thesis supervisor was Eduard Stiefel, but, as Corrado himself likes to recall, it was really Paul Bernays who stimulated his interest in Turing machines and universal computing machines.

Another pioneering result achieved by Corrado Böhm in those years was that of proposing a computing machine for symbolic evaluation. This machine is described in detail, together with the input and output peripherals, in a patent filed in 1952 (Brevetto industriale italiano no. 43.3186).

In 1951 Corrado moved back to Italy. After a period of work at Olivetti-Ivrea in 1953, he became a permanent researcher at the IAC-CNR (Istituto per le Applicazioni del Calcolo – Consiglio Nazionale delle Ricerche) in Rome. At that time the Institute, under the direction of the mathematician Mauro Picone, was involved in a project with Ferranti in Manchester, England, aimed at developing the first (partially Italian) computer, the FINAC (Ferranti-Istituto Nazionale Applicazioni Calcolo). Again Corrado was in charge of the performance evaluation of the computer. To this end he went to Manchester in order to feed FINAC with a system of 63 algebraic equations! Among other contributions to the FINAC, Corrado designed a system called INTINT (INTerpretation-INTegration) for handling vectors.

From 1952 to 1959 Corrado’s main activity at IAC concerned differential and integral calculus and its numerical applications.

The fifties were particularly important years for Corrado also from a personal point of view. In 1950 he married Eva Romanin Jacur, a fascinating lady from Padova and a talented painter. In 1955 their first son Michele was born; in 1958 came their second son Emanuele and in 1960 their daughter Ariela. They are now, respectively, a computer artist, a scholar in oceanography and a sculptor.

It was about this time that Corrado’s work at IAC started moving towards Theoretical Computer Science.

From 1960 to 1968 Corrado continued working at IAC and also lectured in Computer Science at the University of Rome. Giorgio Ausiello, Daniel Bovet, Giuseppe Jacopini, Alfonso Miola, and Marisa Venturni Zilli, among others, were his students at the time. During these years Corrado worked on the theory of Turing machines (14,23). His aim was to apply the theory of Turing machines and recursive functions to programming Von Neumann machines. In 1966 he proved, together with his student Giuseppe Jacopini a seminal result in this area, nowadays known as the Böhm-Jacopini theorem (16). As E.W. Dijkstra puts in a letter to Communications of ACM (11 (3) (1968) 147-148), “(they show) the (logical) superfluousness of the GOTO statement”. The Böhm-Jacopini theorem is considered the theoretical basis of structured programming, the well-known programming style developed and advocated by many researchers in the seventies. This methodology opened a new and more disciplined view of programming and today “programming” really means “programming in a structured way”. More than 200 citations to (16) appear in the literature on “structured programming” of those years. As just one example we mention the book Structured Programming by O.J. Dahl and E.W. Dijkstra and C.A.R. Hoare (Academic Press, New York, 1972).

In the sixties Corrado was one of the first to investigate a new research field in Computer Science: the -calculus. As early as 1963 a dissertation dealing with applications of -calculus to Computer Science was written under his supervision by Marisa Venturini Zilli for her degree in Mathematics; the precise content of this thesis was the representation within -calculus of data types used in Iverson’s language APL. Together with his friend Wolf Gross, Corrado introduced the CUCH, a functional programming language based on Curry’s theory of combinators and Church’s -calculus; see (15, 17). (CUCH is in fact an acronym obtained from the names of these two logicians.) These papers were the starting point of a fruitful research programme, whose aim was to study the properties of functional programming languages by analyzing the properties of paradigmatic abstract languages based on -calculus.

In 1968 Corrado obtained a seminal result in the theory of -calculus, which is nowadays known as Böhm’s theorem (22). What he proved was that two terms of -calculus having syntactically different normal forms with respect to --reduction cannot be consistently equated. In fact, there always exists a context that discriminates between them. This result was proved in order to show soundness of a programming language based on -calculus, like CUCH, where the - and -reduction rules are used as evaluation rules and normal forms are taken as results of computations. Apart from this motivating application, this theorem has been shown to have many important and surprising other consequences, for example the maximality of the theory induced by the standard D -model defined by D. Scott (Continuous lattices, in Lawvere, ed., Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics, Vol. 274 (Springer, Berlin, 1972) 97-136). The importance of Böhm’s theorem lies not only in the result itself, but also in the technique used for proving it, which has been termed the Böhm-out technique in Barendregt’s encyclopaedic book on -calculus; see (The Lambda Calculus, its Syntax and Semantics (North-Holland, Amsterdam, 1984)). The proof of this theorem also suggested to Henk Barendregt a very useful representation of -terms as trees, which he called Böhm trees. Böhm trees have been widely used in the literature and they play an important role in the syntactic and semantic analysis of -calculus.

In 1964 Corrado was one of the promoters of the Working Group 2.2 (Formal Description of Programming Concepts) of IFIP (the International Federation of Information Processing) together with De Bakker, Landin, Scott, Strachey and others. The aim of this group was “to explicate programming concepts through the development, examination and comparison of various formal models of these concepts”. The activities of this group have been extremely influential on later Theoretical Computer Science. For instance, early ideas in formal languages for describing the semantics of programming languages, such as denotational semantics, arose and were thoroughly debated during the meetings of this group. Corrado’s inclusion in this group was an indication of his international standing and of the widely acknowledged relevance of his work. In this period Corrado was established as the leading Italian researcher in the field of Computer Science and one of the most important theoretical computer scientists in the rest of the world.

In 1968 he was appointed as full professor in Computer Science. After a short time spent at the Mathematics Department of the University of Modena, he moved to the University of Turin, where he was appointed head of the project of organizing an undergraduate course in Computer Science in the Faculty of Sciences. (This was only the second project of this kind in Italy, after the one in Pisa, which started in 1969.) Corrado pursued this project with great enthusiasm, notwithstanding the many difficulties due to the lack of resources made available to him by the University. The only computer facility consisted of one IBM 360/44 for the whole of the faculty of Sciences, and the “Computer Science Institute” was located in one single room, which Corrado had to share with all his collaborators. In 1970-71 Corrado met Mariangiola Dezani-Ciancaglini, Mario Coppo, Ines Margaria, Simona Ronchi Della Rocca, and Maddalena Zacchi; all of them had only recently graduated and had been awarded fellowships to do research under Corrado’s supervision. Corrado spent four years in Turin and during this time he was very successful in organizing the Institute and the undergraduate programme. He also succeeded in obtaining improved logistical conditions for his Institute and in convincing the University to devote more financial resources to increasing the computer facilities. He also taught courses on “Systems for Data Processing” and “Formal Languages and Compilers”.

Despite the large amount of time he spent in teaching and organizing during those years, Corrado also did very fruitful research work, establishing in particular a research group in Theoretical Computer Science at the University of Turin. In the field of -calculus, he designed an abstract machine for the call-by-name evaluation of terms, which is interesting for its automatic treatment of -conversion; see (26-28). Moreover he applied the Böhming-out technique to finding solutions for equations between -terms; see (34). In another direction, he started investigating the problem of coding, with integers, families of “information structures”, as he called them, i.e. datatypes, with the aim of saving memory space. Together with Mariangiola Dezani-Ciancaglini and Simona Ronchi Della Rocca he developed coding methods based both on generating functions and on questionnaires (24, 25, 29-33).

In 1974 he moved back to the University of Rome, where he taught “Programming Techniques”. In the same year he organized in Rome an International Conference on Lambda Calculus. This meeting was one of the first to concentrate on this topic and the list of the many open problems collected during the meeting deeply influenced future research; see (36). Some of these were solved only many years later and some are still open. The paper (37), presented at this conference by Corrado (in collaboration with Mariangiola Dezani-Ciancaglini), together with its successor (39), can be considered as the starting point of the intersection type discipline which was developed by the Turin research group during the following years.

In 1975 Corrado also became a member of the Editorial Board of Theoretical Computer Science, a new journal edited by North-Holland, which rapidly became one of the most prestigious European journals on the subject.

It was in the mid-seventies that Corrado started to develop those ideas which have appeared to be central to his studies in recent years. Namely, that normalization is the paradigmatic algorithm and, hence, that the only interesting computations are those that can be coded as strongly normalizing terms. Only programs definable using strictly gauged iterative combinators are amenable to a significant analysis while recursive programs obtained using a brute force application of the fixed point combinator are often not very significant. In this view, Corrado’s research ca be roughly classified into two mainstreams.

First, representation of data structures, and of programs manipulating them, as -terms; representation which are then suitable for writing iterative programs instead of recursive ones.

Second, solutions of equations between -terms and the closely linked separability of problems.

Obviously this classification does not give a full idea of the extent of Corrado’s output in these years (approximately two/thirds of his papers have been published between 1980 and 2000); we will mention only some of the most important results.

In (41, 43) Combinatory Logic is presented as an extension of elementary number theory.

In (46) the notion of minimal form, i.e. of a -term which reduces to itself, was introduced and characterized. This paper was written in collaboration with Silvio Micali, a student of Corrado at the time, who has been honoured with the Gödel award in 1993.

In a series of papers (50, 53, 54, 57, 59, 62), Corrado showed the possibility of replacing recursion by iteration, at the price of changing, in a suitable way, the representation of data structures. The advantage of doing this is that one obtains surely terminating programs.

His research activity on the representation of data structures inside -calculus started with (45). A very important result in this direction was obtained by Corrado in collaboration with Alessandro Berarducci, a student of his, and was presented in (52). It is the automatic translation from the definition of a free algebra, given via the generators, to the representation of the elements of the algebra by means of terms of Girard’s system F (Interprétation Fonctionnelle et élimination des coupures dans l’arithmetique d’ordre supérieur, Thèse de Doctorat d’État, Université de Paris VII, 1972). This representation result can be considered as a cornerstone in the design of functional programming languages.

In collaboration with Adolfo Piperno and Enrico Tronci, he studied the problem of solving equations between -terms and of characterizing invertibility properties of -terms; see (56, 58, 60, 64).

The paper (68) written in collaboration with Benedetto Intrigila proposes the “anti-lion” paradigm. This is a general method for finding strongly normalizable solutions to fixed point equations.

The paper (67) connects his old research on the CUCH machine to his new views on data representations. A very user-friendly functional programming language suitable for writing polymorphic programs is the outcome of this work.

In 1988 a new IFIP working group WG 2.8 (Functional Programming) was established: Corrado was among the promoters. The aim of this WG is “to study the design, implementation and the use of (applicative) functional languages”.

From 1989 to 1991, Corrado was the coordinator of an EEC-funded “ESPRIT” working group, WG 3230, on “Common Foundations of Functional and Logic Programming”. The level of scientific output of this group was very high and the EEC has financed a successor with Corrado as a coordinator, being WG 7232 “Gentzen” (1992-1994).

In 2001 Corrado won the EATCS Award. This prize is awarded in recognition of a distinguished career in theoretical computer science.

Corrado is today active and hard-working as he has always been in his life. He is still greatly in love with Science. He is ready, at any moment, to speculate on general scientific problems as well as to discuss highly technical questions. And this he is ready to do with great enthusiasm with young students as well as senior researchers.

Corrado’s scientific curiosity urges him to seek new fields, like biology and anthropology, but without losing sight of topics studied earlier. We are confident that his future research activity will continue to contribute to the development of Computer Science.

The numbers in the parentheses refer to the numbers in the list of publications.