Corrado Boehm ( Corrado Böhm ; January 17, 1923 , Milan - October 23, 2017 , Rome) - Italian mathematician , specialist in computer science and mathematical logic , who made a decisive contribution to the theoretical substantiation of the structural programming paradigm and obtained important results in λ-calculus , combinatorial logic , semantics of programming languages ; one of the earliest researchers in the theory of programming languages . Professor at the University of Rome " Sapienza ", co-founder of computer science departments at the University of Turin and "Sapienza".
| Corrado Boehm | |
|---|---|
 | |
| Date of Birth | |
| Place of Birth | |
| Date of death | |
| Place of death | |
| A country | |
| Scientific field | |
| Place of work | |
| Alma mater | |
| supervisor | and |
| Awards and prizes | [d] ( 2001 ) |
| Site | |
Biography
Born and raised in Milan . In 1942 he left for Switzerland, where he entered the University of Lausanne . He graduated from the university in 1946 with a degree in electrical engineering , after which he was accepted as an assistant researcher at the Higher Technical School of Zurich [3] .
In 1949–1950, he worked at the Zurich Institute of Applied Mathematics (part of the Zurich Higher Technical School system) in the Edward Stiefel group ( Eduard Stiefel ), and Paul Bernays , who, as the scientist later noted, had It has a great influence, stimulating interest in theoretical issues of computability and Turing machines . Together with another employee of the institute, Harry Laet, he tested the Z4 computer by Konrad Zuse [4] , which was eventually purchased by the Higher Technical School (and thus became the first commercial computer in the world). In 1951, under the leadership of Stiefel, he completed his doctoral thesis, the work was released in 1952, the formal defense took place in 1954.
In 1950, he married an artist from Padua, Eva Romanin Yakur, and in 1951 he returned to Italy. In 1953, he worked in Ivrea at Olivetti , and in the same year was accepted as a researcher at the Institute of Applied Mathematical Analysis ( Italian: Istituto per le applicazioni del calcolo ) in Rome . At the institute, together with the British company Ferranti, under the leadership of Mauro Picone ( Italian: Mauro Picone ), the first Italian computer , and Böhm was engaged in testing its performance [3] . Basically, the works of the period of the 1950s are devoted to the main direction of the institute - differential and integral calculus and its applications. In the second half of the 1950s, three daughters were born in a marriage with Eve.
Since 1960, while continuing to work at the Institute of Applied Mathematical Analysis, he began to teach computer science courses at the Sapienza University of Rome , and the first graduate students appeared there. In 1968 he received a professorship.
Since 1969 - the head of the informatics course at the Faculty of Science of the University of Turin , in 1974 he returned to Rome in “Sapienza”. In 1975, he organized an international conference on λ-calculus at the university, which became the first such event in the direction and played an important role in its rapid development in the next decade. In the same year he entered the editorial board of the journal , which remained until the last years; To the 70th anniversary of the scientist in 1993, the magazine devoted a special issue.
In 1990 he was elected academician of the European Academy [5] . In 1994 received the degree of honoris causa of the University of Milan [6] . In 2001, he was awarded the European Association of Theoretical Informatics ( English EATCS Award ) [7] for achievements in the field of the theory of programming languages.
Scientific contribution
As part of his dissertation, he created the language and a compiler for it. The main innovation was that the language compiler was developed in the same language itself, that is, it became the first complete metacircular compiler in the history ( eng. Meta-circular compiler ) [8] . The compiler text took only 114 lines of code .
In 1964, he created the programming language P ′ ′ , a minimalistic language without an unconditional jump operator . In support of the computational expressiveness of the created language, in collaboration with one of the students at the Sapienza University, Giuseppe Jakopini, in 1966 proved the turing completeness of P ′ ′, which in turn meant the expressibility of any algorithm by only three control structures — sequential transmission control, branching and looping . This result summed up the scientific basis for structured programming: in a 1968 note, Dijkstra referred to the Böhm – Jakopini theorem as an opportunity to completely eradicate the GOTO operator from programming practice [9] , after which the paradigm was universally recognized.
From the mid-1960s, he worked on the problems of λ-calculus. Among the results obtained is the contradictory theorem on the equivalence of various λ-terms in -normal form (i.e. not having undisclosed sub-terms of the form and where is not a free variable in ). From this statement immediately follows the Hilbert completeness - Post extensional λ-calculus . In addition to the importance of the result itself, methods for proving the assertion also turned out to be in demand: the Böhm’s technique of inverting terms used Barendregt to compare each term of the construction, which he called the Böhm tree , remarkable for the fact that all definable λ-calculus functions on these trees are continuous [10] . Another work in the field of λ-calculus that influenced the theory of programming languages was the construction of an abstract machine with the strategy of computing a call by name with automatic processing in the early 1970s with student Marianjola Dedzani-Chankaglini ( Italian: Mariangiola Dezani-Ciancaglini ). conversions.
Selected bibliography
- C. Böhm. Calculatrices digitales. Di déchiffrage des formules logico-mathématiques par la machine de mécément conception program // Annali di Matematica Pura ed Applicata. - 1954. - T. 37 , No. 4 . - pp . 175-217 .
- C. Böhm. On a family of Turing machines and related programming language // International Computer Center Bulletin. - 1964. - T. 3 , No. 3 . - publication about P ′ ′
- C. Böhm, G. Jacopini. Flow diagrams, Turing machines and languages with only two formation rules // Communications of the ACM . - 1966. - T. 5 , No. 9 . - p . 366-371 . - article with Boehm – Jakopini theorem
- C. Böhm. Alcune proprietà delle forme normali nel calcolo // Publicazioni del'Istituto per le applicazioni del calcolo. - No. 696 . - article with Böhm theorem on the separability of terms in normal form and containing the technique of inversion of terms
- C. Böhm, M. Dezani-Ciancaglini. Can syntax be ignored during translation? // Automata, Languages and Programming / M. Nivat. - Amsterdam: North-Holland, 1972. - p . 197-207 . - an article about the calculation strategy with calling by name with automatic conversion
- λ-Calculus and Computer Science Theory / C. Böhm (editor). - Berlin: Springer-Verlag, 1975 .-- T. 37 .-- 383 p. - (Lecture Notes in Computer Science). - ISBN 3-540-07416-3 . - materials of the symposium on λ-calculus in computer science, which was held March 25-27, 1975
Notes
- ↑ 1 2 http://www.corradobohm.it/Corrado_Bohm/Biography.html
- ↑ http://www.cnrs.fr/ins2i/spip.php?article2697
- ↑ 1 2 Biography, 2013 .
- ↑ Herbert Bruderer. Computing History Beyond the UK and US: Selected Landmarks from Continental Europe // Communications of the ACM. - 2017. - T. 60 , No. 2 . - pp . 76-84 . - DOI : 10.1145 / 2959085 .
- ↑ Corrado Böhm . Academia Europaea (October 24, 2017). The appeal date is January 8, 2018.
- ↑ In memoria di Corrado Böhm (1923-2017) . Università degli Studi di Roma "La Sapienza" (October 23, 2017). The appeal date is January 8, 2018.
- ↑ EATCS Award . European Association of Theoretical Computer Science (January 1, 2018). The appeal date is January 8, 2018.
- ↑ Donald E. Knuth, Luis Trabb Pardo. The Early Development of Programming Languages // The Metropolis, I. Howlett, Gian-Carlo Rota. - NY: Academic Press. - pp . 200-276 . - ISBN 0-12-491650-3 .
- ↑ E. Dijkstra. Go to statement considered harmful // Communications of the ACM . - 1968. - T. 11 , No. 3 . - p . 147–148 . - DOI : 10.1145 / 362929.362947 .
- ↑ Barendregt, Henk . Chapter 10. Boehm Trees // Lambda Calculus. Its syntax and semantics = The Lambda Calculus. Its syntax and semantics (Russian) / translation from English by G. E. Mints. - M .: Mir , 1985. - S. 19, 46, 220-267. - 606 s. - 4800 copies
Links
- Corrado Böhm's bio and bibliography . corradobohm.it (January 26, 2013). The appeal date is January 7, 2017.