Типізоване лямбда-числення — це система лямбда-числення, у якій кожний вислів має тип. У цьому контексті тип — це формула певної системи числення, як-от (інтуїціоністської) пропозиційної логіки або логіки першого порядку. Типізоване лямбда-числення з простими типами (де типи — це формули імплікаційного фрагменту інтуїціоністської логіки) має застосування на практиці в функціональних мовах програмування, наприклад Haskell. Складніші типізовані системи є важливими для вивчення загальних характеристик обчислюваності та у сфері автоматизації автоматичних доведень.
Див. також Система F
Посилання