Коррадо Бём (17 января 1923 — 23 октября 2017) — итальянский учёный-компьютерщик и почётный профессор Римского университета «Ла Сапиенца» , особенно известный своим вкладом в теорию структурного программирования , конструктивной математики , комбинаторной логики , лямбда-исчисления . а также семантика и реализация языков функционального программирования .
В своей докторской диссертации (по математике, в ETH Zurich, 1951; опубликована в 1954 году) Бём впервые описывает полный метациклический компилятор , то есть механизм перевода языка программирования, написанный на этом же языке. Его наиболее влиятельным вкладом является так называемая теорема о структурированной программе , опубликованная в 1966 году совместно с Джузеппе Якопини. Вместе с Алессандро Берардуччи он продемонстрировал изоморфизм между строго положительными алгебраическими типами данных и полиморфными лямбда-термами, также известным как кодирование Бема – Берардуччи. [1]
В лямбда-исчислении он установил важную теорему разделения между нормальными формами, известную как теорема Бёма, которая утверждает, что для каждых двух замкнутых λ-членов T 1 и T 2 , имеющих разные βη-нормальные формы, существует терм Δ, где Δ T 1 и Δ T 2 оценивают разные свободные переменные (т. е. их можно внутренне разделить). Это означает, что для нормализующих терминов контекстуальная эквивалентность Морриса , которая является семантическим свойством, может быть определена через равенство нормальных форм, синтаксическое свойство, поскольку оно совпадает с βη-равенством.
В 1993 году, к его 70-летию, ему был посвящен специальный выпуск журнала Theoretical Computer Science . Он является лауреатом премии EATCS 2001 года за выдающуюся карьеру в области теоретической информатики.