题目：Dependent Type Theories and Mathematical Pluralism
主讲人： 罗朝晖 （伦敦大学教授）
时间：2007年12月12日（周三）下午2:00-4:00
地点： 中国人民大学人文楼六层会议室（六层电梯出口对面）
讲座提要：

 Dependent type theories provide powerful foundational calculi for formalisation and logic reasoning. In this talk, I shall first give an introduction to the modern development of type theory and its applications to the foundational study and to the technology of interactive theorem proving.

Then, the type-theoretic framework LTT is (informally) presented. LTT provides a uniform foundational calculus for mathematical reasoning with deferent logic foundations. This, among things, establishes the basis for “mathematical pluralism”, a pragmatic position in the foundations of mathematics.