Basic track

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.

Read more…

λ-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…

Comments are closed.