Institute of Information Science Academia Sinica
Topic: Termination of higher-order rewrite systems using the notion of computability closure
Speaker: Dr. Hab. Frédéric Blanqui (INRIA)
Date: 2012-11-16 (Fri) 10:00 – 12:00
Location: Auditorium 106 at new IIS Building
Host: Bow-Yaw Wang


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.