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 room V005a | Tuesday 2 July room V005a | Wednesday 3 July room V005a | Thursday 4 July room V106b | Friday 5 July room L226 | Saturday 6 July room V005a | |
|---|---|---|---|---|---|---|
| 8:15 | registration | |||||
| 8:30 | coffee room V334 | coffee room V334 | coffee room V334 | coffee room V106a | coffee room V334 | |
| 8:45 | introduction | |||||
| 9:00 | lecture on rewriting | lecture on rewriting | lecture on rewriting | lecture on rewriting | lecture on rewriting | coffee room V106b |
| 9:15 | exam on rewriting (optional) | |||||
| 10:30 | break | break | break | break | break | |
| 10:45 | break | |||||
| 11:00 | lecture on rewriting | lecture on rewriting | exercises on rewriting | lecture on rewriting | exercises on rewriting | λ-calculus |
| 12:30 | lunch | lunch | lunch | lunch | lunch | lunch |
| 14:00 | lecture on rewriting | exercises on rewriting | lecture on rewriting | exercises on rewriting | λ-calculus | λ-calculus |
| 15:30 | break | break | break | break | break | break |
| 16:00 | exercises on rewriting | lecture on rewriting | social event | lecture on rewriting | λ-calculus | end |
| 17:30 | break | break | free time | break | break | |
| 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) | end | ||
| 18:30 | cocktail | |||||
| 19:30 | end | end | end | |||
| 20:00 | diner |
First-order term rewriting
| 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.
λ-calculus
| 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.
Read more…