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.
