# 6th International School on Rewriting

# July 16th - 20th, 2012. Valencia, Spain

## LCA: Lambda Calculus: Extensions and Applications

Lambda calculus is a higher-order rewriting system created by Alonzo Church in 1936 to describe functions. Unlike first order rewriting systems, lambda calculus has binders. We will present the lambda calculus and prove that it is confluent (no ambiguities) . We will look at type systems for lambda calculus and prove that the rewriting system is terminating on typed terms.