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 want 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||coffee|
|9:15||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||social event||lecture on rewriting||λ-calculus||end|
|18:00||Short talks session||Deduction modulo rewriting|
Gilles Dowek (advanced track)
|Formal specification and analysis of real-time systems in Real-Time Maude|
Peter Csaba Ölveczky (advanced track)
|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.