Time:  12:30  13:30 
Room: 
Wean Hall 8220

Speaker: 
Rick Statman Department of Mathematics CMU 
Title: 
An introduction to λcalculus

Abstract: 
λcalculus is that branch of logic which employs algebraic methods to study computer programs and the resulting computable functions. Conventional algebraic structures such as groups and fields are normally absent, and unconventional structures such as Cartesian monoids and nearrings take their place. The object is to classify computer programs and the functions they compute by their functional/algebraic properties such as typeability; f: D > R and invariance; P(f) = f. The first lecture will give an introduction to λcalculus à la Rocquencourt. The basic theorems of reduction and conversion will be discussed,including ηconversion,and the SchönfinkelCurry theory of combinators will be introduced. The second lecture will describe several algebraic structures, including Cartesian monoids and nearrings, which occur in λcalculus. 