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
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
,
combinatory logic,
lambda calculus, and the semantics and implementation of
functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...
languages.
Work
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
The structured program theorem, also called the Böhm–Jacopini theorem, is a result in programming language theory. It states that a class of control-flow graphs (historically called flowcharts in this context) can compute any computable function ...
, published in 1966 together with Giuseppe Jacopini. Together with Alessandro Berarducci, he demonstrated an isomorphism between the strictly-positive
algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., ...
s and the polymorphic lambda-terms, otherwise known as Böhm–Berarducci encoding.
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 T
1 and T
2 which have different βη-normal forms, there exists a term Δ where Δ T
1 and Δ T
2 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
* 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ürichEnglish 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
In computability theory, a system of data-manipulation rules (such as a computer's instruction set, a programming language, or a cellular automaton) is said to be Turing-complete or computationally universal if it can be used to simulate any ...
.
* 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
* P′′, a minimal computer programming language
* Structured program theorem
The structured program theorem, also called the Böhm–Jacopini theorem, is a result in programming language theory. It states that a class of control-flow graphs (historically called flowcharts in this context) can compute any computable function ...
* List of pioneers in computer science
This is a list of people who made transformative breakthroughs in the creation, development and imagining of what computers could do.
Pioneers
: ''To arrange the list by date or person (ascending or descending), click that column's small "up-do ...
* Böhm tree
* Böhm's theorem
References
Vitae (University of Rome)
External links
*
''Theoretical Computer Science'', Volume 121, Numbers 1&2, 1993.
Corrado Böhm's personal page
1923 births
2017 deaths
Italian computer scientists
Sapienza University of Rome faculty
Italian people of German descent
École Polytechnique Fédérale de Lausanne alumni
20th-century Italian scientists
21st-century Italian scientists
Scientists from Milan
{{compu-scientist-stub