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