Corrado Böhm (17 de enero de 1923 - 23 de octubre de 2017) fue un científico informático italiano y profesor emérito de la Universidad de Roma "La Sapienza" , conocido especialmente por sus contribuciones a la teoría de la programación estructurada , las matemáticas constructivas , la lógica combinatoria , el cálculo lambda y la semántica e implementación de lenguajes de programación funcional .
En su tesis doctoral (en Matemáticas, en la ETH de Zúrich, 1951; publicada en 1954), Böhm describe por primera vez un compilador metacircular completo , es decir, un mecanismo de traducción de un lenguaje de programación, escrito en ese mismo lenguaje. Su contribución más influyente es el llamado teorema del programa estructurado , publicado en 1966 junto con Giuseppe Jacopini. Junto con Alessandro Berarducci, demostró un isomorfismo entre los tipos de datos algebraicos estrictamente positivos y los términos lambda polimórficos, también conocidos como codificación de Böhm-Berarducci. [1]
En el cálculo lambda , estableció un importante teorema de separación entre formas normales, conocido como teorema de Böhm, que establece que por cada dos términos λ cerrados T 1 y T 2 que tienen diferentes formas βη-normales, existe un término Δ donde Δ T 1 y Δ T 2 evalúan diferentes variables libres (es decir, pueden separarse internamente). Esto significa que, para los términos normalizadores, la equivalencia contextual de Morris , que es una propiedad semántica, puede decidirse a través de la igualdad de las formas normales, una propiedad sintáctica, ya que coincide con la βη-igualdad.
En 1993, con motivo de su 70.º cumpleaños, se le dedicó un número especial de Theoretical Computer Science . Recibió el premio EATCS 2001 por su destacada trayectoria en el campo de la informática teórica.