Corrado Böhm

From Wikipedia, the free encyclopedia

Corrado Böhm
CorradoBoemETAPS2013 2013-03-22 0.33.36.jpg
Corrado Böhm's 90th birthday celebration at ETAPS 2013 in Rome, Italy
Born(1923-01-17)17 January 1923
Died23 October 2017(2017-10-23) (aged 94)
NationalityItalian
Alma materETH Zürich
Scientific career
FieldsComputer science
InstitutionsUniversity of Rome "La Sapienza"
Doctoral advisor
Doctoral students

Corrado Böhm (17 January 1923 – 23 October 2017) was a Professor Emeritus at the University of Rome "La Sapienza" and a computer scientist known especially for his contributions to the theory of structured programming, constructive mathematics, combinatory logic, lambda calculus, and the semantics and implementation of functional programming languages.

Work[edit]

In his PhD dissertation (in Mathematics, at ETH Zurich, 1951; published in 1954), Böhm describes for the first time a full meta-circular compiler, that is a translation mechanism of a programming language, written in that same language. His most influential contribution is the so-called structured program theorem, published in 1966 together with Giuseppe Jacopini. Together with Alessandro Berarducci, he demonstrated an isomorphism between the strictly-positive algebraic data types and the polymorphic lambda-terms, otherwise known as Böhm–Berarducci encoding.[1]

In the lambda calculus, he established an important separation theorem between normal forms, known as Böhm's theorem, which states that for every two closed λ-terms T1 and T2 which have different βη-normal forms, there exists a term Δ where Δ T1 and Δ T2 evaluate to different free variables (i.e., they may be taken apart internally). This means that, for normalizing terms, Morris' contextual equivalence, which is a semantic property, may be decided through equality of normal forms, a syntactic property, as it coincides with βη-equality.

A special issue of Theoretical Computer Science was dedicated to him in 1993, on his 70th birthday. He is the recipient of the 2001 EATCS Award for a distinguished career in theoretical computer science.

Selected publications[edit]

  • C. 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, serie IV, tomo XXXVII, 1–51, 1954. PDF at ETH Zürich English translation 2016 by Peter Sestoft
  • C. Böhm, "On a family of Turing machines and the related programming language", ICC Bull., 3, 185–194, July 1964.
    Introduced P′′, the first imperative language without GOTO to be proved Turing-complete.
  • C. Böhm, G. Jacopini, "Flow diagrams, Turing Machines and Languages with only Two Formation Rules", Comm. of the ACM, 9(5): 366–371,1966.
  • C. Böhm, "Alcune proprietà delle forme β-η-normali nel λ-K-calcolo", Pubbl. INAC, n. 696, Roma, 1968.
  • C. Böhm, A. Berarducci, "Automatic Synthesis of typed Lambda-programs on Term Algebras", Theoretical Computer Science, 39: 135–154, 1985.
  • C. Böhm, "Functional Programming and Combinatory algebras", MFCS, Carlsbad, Czechoslovakia, eds M.P. Chytil, L. Janiga and V. Koubek, LNCS 324, 14–26, 1988.

See also[edit]

References[edit]

  1. ^ "Boehm-Berarducci Encoding".

External links[edit]