Corrado Böhm (17 January 1923 – 23 October 2017) was an Italian
computer scientist
A computer scientist is a scientist who specializes in the academic study of computer science.
Computer scientists typically work on the theoretical side of computation. Although computer scientists can also focus their work and research on ...
and Professor
Emeritus
''Emeritus/Emerita'' () is an honorary title granted to someone who retires from a position of distinction, most commonly an academic faculty position, but is allowed to continue using the previous title, as in "professor emeritus".
In some c ...
at the
University of Rome "La Sapienza", known especially for his contributions to the theory of
structured programming Structured programming is a programming paradigm aimed at improving the clarity, quality, and development time of a computer program by making specific disciplined use of the structured control flow constructs of selection ( if/then/else) and repet ...
,
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
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of com ...
,
lambda calculus
In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
, and the semantics and implementation of
functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...
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, 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 data type, i.e., a data type formed by combining other types.
Two common classes of algebraic types are product ty ...
s and the polymorphic lambda-terms, otherwise known as Böhm–Berarducci encoding.
In the
lambda calculus
In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
, 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
*
*: 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 model of computation, 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 ...
.
*
*
*
*
See also
*
P′′, a minimal computer programming language
*
Structured program theorem
*
List of pioneers in computer science
*
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
Academic staff of the Sapienza University of Rome
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