Constructive Type Theory by Terkia Mechouet, Farid Zidani

“…among them Russell’s Type Theory, which is founded on the concept of type, despite its imperfections and criticisms, opened the way to others theories like the Alonzo Church’s one which is based on function not on set, and built what we call Lambda Calculus in 1930. These theories were the origin of Constructive Type theory and its basic concepts: type, proposition, judgment, proof…etc. …”
Get full text