Termination of higher-order rewrite systems using the notion of computability closure
- 講者Hab. Frédéric Blanqui 博士 (INRIA)
邀請人:王柏堯 - 時間2012-11-16 (Fri.) 10:00 ~ 12:00
- 地點資訊所新館106演講廳
摘要
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.