Page under construction!…

The basic track provides an introduction to first-order term rewriting and λ-calculus.

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.

### λ-calculus

Femke van Raamsdonk (VU University Amsterdam) |

Page under construction!…