El cálculo lambda simplemente tipado es una teoría de tipos basada en el cálculo de lambda con un único constructor de tipos, , que construye tipos función. Es el ejemplo canónico y más sencillo de un cálculo lambda tipado. El cálculo lambda simplemente tipado fue originalmente introducido por Alonzo Church en el 1940 como un intento de evitar la aparición de paradojas en el cálculo lambda sin tipos.