|
Courses and Workshops
|
| Title: | Nominal techniques for reasoning about formal languages |
| Lecturer(s): | Christian Urban (University of Cambridge) |
| Type: | Advanced Course |
| Section: | Logic and Computation |
| Week: | Second | | Time: | 11.00-12.30 (Slot 2) |
| Webpage: | http://www.cl.cam.ac.uk/~cu200
|
| Reader: | Download | | Room: | C2 |
Description When reasoning about formal languages, dealing with binding constructs
is often delicate and error-prone, in particular when proving properties
by structural induction. This course describes a general framework for
representing formal languages involving binders and reasoning modulo
renaming of bound names. The framework is based on the operation of
swapping of names and on the notion of equivariant predicates (that is
predicates that are invariant under the swapping operation); the
framework provides rigorous proving techniques that are pleasantly close
to informal practice, in contrast with more sophisticated techniques
such as de-Bruijn indices and higher-order abstract syntax. Examples
explaining the techniques will be drawn from the lambda-calculus.
|
© 2003, 2004 LORIA, Carlos Areces. |
2004-07-05
| |
