LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
2pm, Wednesday 19th March 1997

*NOTE NONSTANDARD DAY AND TIME*

Title: Coercive subtyping and its applications

Speaker: Zhaohui Luo (University of Durham)

Coercive subtyping offers a conceptually simple but powerful framework to understand subtyping and subset relationships in type theories with sophisticated type structures such as dependent types and inductive types. In this talk, we introduce the basic concepts and some of its applications. In particular, I shall explain its use in the design of a mathematical vernacular for computer-assisted reasoning with natural language.