Termination of higher-order rewrite systems using the notion of computability closure
- LecturerDr. Hab. Frédéric Blanqui (INRIA)
Host: Bow-Yaw Wang - Time2012-11-16 (Fri.) 10:00 ~ 12:00
- LocationAuditorium 106 at new IIS Building
Abstract
I will recall the notion of computability introduced by W. W. Tait and J.-Y. Girard for proving the termination of beta-reduction in typed lambda-calculi, and show how it can be extended to deal with various forms of higher-order rewrite relations, and how it can be related with other notions or techniques too.