Типізоване лямбда-числення: відмінності між версіями

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