Introduction To Lambda Calculus

ABOUT THE COURSE:This course offers an introductory overview of lambda calculus, which serves as the basis for various functional programming languages such as Haskell. In the initial two weeks, we focus on fundamental concepts like function representation, function abstraction and application, and term reduction (i.e., computation). A particular emphasis is placed on the creation of complex functions and data structures from the ground up, a topic often overlooked in most textbooks and online resources. The following two weeks will address simply typed lambda calculus. We will establish a formal system that allows us to logically deduce that a term M possesses a type \tau . An algorithm for assigning principal types to typable terms will be demonstrated through examples. Lastly, we will briefly explore the idea of the relationship between types as logical formulas and the proofs of these logical formulas as type deductions of lambda terms.INTENDED AUDIENCE: UG/PG/PhD students in CSEPREREQUISITES: No pre-requisites are required regarding attending any other course(s) before taking this course. MathJax.Hub.Typeset();

Syllabus

Week 1: Representation of a function in anonymous mode, partial application of functions, Currying technique, Syntax of pure Lambda calculus, technique for removal of redundant parenthesis from a lambda term, Free and bound variables, reductions, Church-Rosser Theorem, Normal forms, call-byname, call-by-value semantics.
Week 2:Representation of if-then-else, recursion, Y combinator, Church numerals, synthesis of some arithmetic functions (successor function, iszero, plus, multiply) and Boolean operations (or, and, not, exclusive or)
Week 3:Simply typed lambda calculus, the type system TA λ: motivation and definitions, work out examples of how deduction is done in the system, construction tree of term and type: work out some examples
Week 4:Principal Type algorithm, substitution, most general unifier, work out some examples of the working of the algorithm, Intuitionistic implicational logic, Curry-Howard isomorphism