Redigerer Typeteori (avsnitt)

=== Lambdakalkyle à la Curry ===
Presentasjonen av <math>\lambda^\to</math> i avsnittene over, er presentert à la Church, siden termene er annotert med typer. Et alternativ er å beholde de utypede termene fra den 
utypede lambdakalkylen. Dette kalles à la Curry, og definisjonen av termer er da:
:<math> e ::= x \mid \lambda x . e \mid e \, e </math> 
og typerelasjonen er
{| align="center" cellpadding="9"
| align="center" | <math> { \Gamma(x) = \tau \over \Gamma \vdash x : \tau } </math> (var)
| align="center" | <math> { \Gamma \vdash e_1 : \tau_2 \to \tau_2 \quad \Gamma \vdash e_2 : \tau_2 \over \Gamma \vdash e_1 \, e_2 : \tau_2} </math> (app)
| align="center" | <math> { \Gamma, x : \tau_2 \vdash e : \tau_2 \over \Gamma \vdash \lambda x . e : \tau_1 \to \tau_2 } </math> (lam)
|}

Hvorvidt et typesystem er presentert à la Curry eller Church vil få følger for hvilke egenskaper systemet får. F.eks. kan et uttrykk <math>e</math> i <math>\lambda^\to</math> à la Church kun
ha en type, mens i à la Curry kan et term ha mange forskjellige typer. For mer uttrykksfulle typesystemer, så kan typesjekking bli uavgjørbart i Curry form, mens de oftere er avgjørbare i Church form. 
Noen typesystemer har kun mening i en av formuleringene.