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