The basic track provides an introduction to first-order term rewriting (25.5 hours) and λ-calculus (6 hours). An exam (1.5 hour, optional) will be organized for the participants who needs it to get credits in their university.
|Monday 1 July||Tuesday 2 July||Wednesday 3 July||Thursday 4 July||Friday 5 July||Saturday 6 July|
|9:00||lecture on rewriting||lecture on rewriting||lecture on rewriting||lecture on rewriting||lecture on rewriting||exam on rewriting (optional)|
|11:00||lecture on rewriting||lecture on rewriting||exercises on rewriting||lecture on rewriting||exercises on rewriting||λ-calculus|
|14:00||lecture on rewriting||exercises on rewriting||lecture on rewriting||exercises on rewriting||λ-calculus||λ-calculus|
|16:00||exercises on rewriting||lecture on rewriting||lecture on rewriting||λ-calculus|
|Aart Middeldorp (Innsbruck University)||Sarah Winkler (Innsbruck University)|
Term rewriting is a conceptually simple, but powerful abstract model of computation which underlies much of declarative programming and automated theorem proving. The foundation of rewriting is equational logic. It constitutes a basic framework for program analysis and has applications in automated reasoning, algebra, computability theory and lambda calculus, compiler construction, engineering, as well as functional and logic programming.
This course provides a modern introduction to rewriting in general and term rewriting in particular. All key concepts are covered and glimpses into current research will be provided. Moreover, several automatic tools will be demonstrated.
|Femke van Raamsdonk (VU University Amsterdam)|
The λ-calculus is originally introduced by Church to study the foundations of mathematics. λ-terms with β-reduction form a Turing-complete model of computation.
In this course we will discuss some subjects in the rewriting theory of λ-calculus. Every lecture will have the following structure: lecture, time to work individually on a few exercises, wrap-up.