Research Project

Subtyping, Inheritance, and Reuse:
Developing Expressive Type Theory for Formal Analysis

Zhaohui Luo and Keith Bennett
Dept of Computer Science, University of Durham

Funded by EPSRC, grant ref. GR/K79130 (Oct. 1996 -- Feb. 2000)
In collaboration with R. Burstall at Edinburgh and DSE Ltd.

Type theory has emerged as an important technology for computer-assisted formal reasoning. Exploiting the parallel between propositions and types and that between proofs and programs, proof systems based on type theory have proved to be useful and suitable for formalising and analysing systems. The research in this area has so far achieved notable success both in the advance of expressive type theories and in development of proof systems. With the basic technology in place, an important aim of current research is to make type theory and the associated tools more effective for industrial scale development problems.

Our aim is to make large-scale formal analysis easier. It is widely recognised that effective reuse is essential for formal analysis of large systems to become feasible. However, unlike object-oriented languages, the current expressive type theories (with inductive types and module mechanisms) do not provide effective means such as subtyping to support direct inheritance and reuse of developed formal theories and proofs, and experience of large development has shown that further development is needed to solve this problem.

This research project is to address this by developing subtyping and inheritance mechanisms for expressive type theories and studying reuse methods in the context of computer-assisted formal reasoning. Our previous work on type theories ECC and UTT [1] and the development of the Lego proof development system [2] has established a good basis for the current project. For example, modular methods have been studied for structuring and developing generic formal theories, which may be used in many different contexts of formal development.

The project focuses on further development of expressive type theory by introducing suitable subtyping mechanisms to provide more powerful ways of reasoning such as inheritance of proof principles, and studying how subtyping can be combined with existing inductive types and module mechanisms to support direct inheritance of formal theories and proofs. The Lego system will be used as an experimental platform to develop support for subtyping and inheritance. We expect the subtyping theory and the associated inheritance methods to lead to new techniques for effective proof development and to make contributions of long-term importance to the theory and practice of interactive theorem proving.

Research on Coercive Subtyping: Project Summary

In this project, we have developed coercive subtyping, a new theory of subtyping and inheritance for type theories, especially those with dependent types and inductive types. We have developed the logical framework for coercive subtyping, studied its meta-theoretic properties, implemented the framework in a new theorem proving system Plastic, and considered various aspects of its applications.

The project is extremely successful. It has led to significant advances of the theory of subtyping and inheritance and its associated technology for formal development. Besides developing the framework and its implementation and applications, we have successfully studied difficult technical issues for the theory of coercive subtyping with results that justify the theory and its implementations.

See below ([3] -- [12]) for some of the publications produced in this project.

Related personnel

References and related papers

[1] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science, 11. Oxford University Press, 1994. (ISBN 0 19 853835 9)

[2] Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. ECS-LFCS-92-211, Dept of Computer Science, Edinburgh Univ, 1992. [dvi file available.]

[3] Z. Luo. Coercive subtyping in type theory. Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, 1997. [dvi and ps files available.]

[4] Z. Luo. Coercive subtyping. Journal of Logic and Computation. Vol. 9, No. 1. 1999 [ps file available.]

[5] Z. Luo and P. Callaghan. Coercive subtyping and lexical semantics (extended abstract). Logical Aspects of Computational Linguistics (LACL'98), Grenoble, 1998. [ps file available.]

[6] A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. Types for proofs and programs, (eds.) E. Gimenez and C. Paulin-Mohring. LNCS 1512. [ps file available.]

[7] Z. Luo and P. Callaghan. Mathematical vernacular and conceptual well-formedness in mathematical language. Proceedings of the 2nd Inter. Conf. on Logical Aspects of Computational Linguistics (LACL'97), Nancy. LNCS/LNAI 1582. [ps file available.]

[8] S. Soloviev and Z. Luo. Coercion completion and conservativity in coercive subtyping. 1999. Annals of Pure and Applied Logic, to appear.

[9] P. C. Callaghan. Coherence checking and its implementation in plastic. APPSEM Workshop on Subtyping and Dependent Types in Programming, 2000.

[10] P.C. Callaghan and Z. Luo. Implementation techniques for inductive types. Proceedings of TYPES'99, 1999.

[11] P.C. Callaghan and Z. Luo. Plastic: an implementation of typed LF with coercive subtyping and universes. 2000

[12] Z. Luo and S. Soloviev. Dependent coercions. Proc of the 8th Inter. Conf. on Category Theory in Computer Science (CTCS'99), Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science, Vol 29, 1999. [ps file available.]
Zhaohui.Luo at rhul.ac.uk