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 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)

10:30

break

break

break

break

break

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

social event

break

break

16:00

exercises on rewriting

lecture on rewriting

lecture on rewriting

λ-calculus

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.