The idea of a language that includes Curry combinators and Church lambda calculus was first presented in the paper of Böhm and Gross ”Introduction to the CuCh” in 1966 (formerly in a paper of 1964) and an algorithm that allows the reduction of any CuCh term to a normal form  was elucidated in a paper with Mariangiola Dezani ”The CuCh machine: The automatic treatment of bound variables” in June 1972.

Then in the late 80s Corrado undertook the project of realizing a new CuCh Machine. Several students of Corrado helped him in this project, in particular Stefano Guerrini and Luigi Mazzucchelli.

The CuCh both as a formal and description language and as a machine, represents:

• A formal framework for the synthesis of the Curry combinatory logic and the Church

• λ-calculus in a set of well-proven mathematical settings

A proven and fertile approach that progressed for over 50 years of research and implementations, from key papers in theoretical computer science to one of the first examples of cross-platforms functional languages with one of the smallest footprint on the market and wider range of deployments.

the CuCh machine was recently ported in Android. IoS version is currently under development.

Older versions - from DOS, Macbook, Windows executables, Java API, .... are available as executable files as well as in Virtual Machines - ready to run. 

Please stay tuned. A dedicated page with downloads in different executable formats and VMs is about to be published.

Corrado Böhm had deeply influenced the development of theoretical Computer Science. In Corrado's PhD thesis in 1954 a language, a machine and a compiler were designed together for the first time. No compiler was written in its own language before. The seminal result is nowadays known as the Böhm-Jacopini theorem that has been set as a theoretical basis of structured programming, opening the way to all generations of modern programming languages. In the 19-sixties, Corrado was one of the first scientists to investigate the link between λ-calculus and theoretical computer science, a fruitful research field which later became established as the foundation of programming language semantics. The Bohm's theorem suggested the representation of λ-terms as Bohm trees, widely used in the literature. His work and ideas have been strongly infuential in the domain of lambda calculus and its applications to programming but also, more generally, for the whole field of programming theory.

The notable Curry-Curch machine (CuCh) was defined and developed and consitutes one of the eritages of Corrado's work. On the occasion of his 70-th and 90-th birthday, the international Computer Science community dedicated to Corrado Bohm two volumes of international journals.

In 2001 he was awarded in recognition of a distinguished career in theoretical computer science by the European Association for Theoretical Computer Science, EATCS AWARD. Corrado always worked with an amazing enthusiasm, generosity and curiosity.

Corrado Bohm, born 17th of January 1923 in Milano, passed away 23rd of October 2017 in Rome.