Title: Formalisation and Verification in a Type-theoretic Framework

Speaker: Prof. LUO Zhaohui £¨Dept of Computer Science, Royal Holloway, Univ
of London£©

Time: 3pm, Tuesday Dec. 11

Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute
of Software, CAS

Abstract:

Dependent type theory provides a powerful logical calculus for computer-assisted
formal reasoning. The associated technology of theorem proving has produced
very useful tools, the so-called ¡°proof assistants¡±, for formal proof development
both in the verification of programs and in the formalisation of mathematics.After
giving an overview of the research field, I shall present a new type-theoretic
framework LTT and explain its use in formalisation and verification. The particular
features of the LTT framework include:v LTT is a foundational calculus for formal
reasoning with different logical foundations, establishing the basis for wider
applications of the type theory based theorem proving technology. v LTT employs
a notion of ¡°typed set¡±, combining the type-theoretical reasoning with the set-theoretical
reasoning in an effective way and supporting efficient proof development in
formalisation and verification. As a promising framework, LTT has been used
in several case studies, including the formalisation of Weyl¡¯s predicative mathematics
and the analysis of security protocols.

.