Abstract
Coercive subtyping is a general approach to subtyping, inheritance and abbreviation in dependent type theories. A vital requirement for coercive subtypingis that of coherence - computational uniqueness of coercions between any two types. In this paper, we develop techniques useful in provingcoherence and its related result on admissibility of transitivity and substitution. In particular, we consider suitable subtyping rules for Π-types and ∑-types and prove its coherence and the admissibility of substitution and transitivity rules at the type level in the coercive subtypingframework.
The first author thanks the support of the ORS Award and the Durham University studentship. This work by the second author is partly supported by the UK EPSRC grant GR/M75518 and the EU grant on the TYPES project.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
B. Barras et al. The Coq Proof Assistant Reference Manual (Version 6.3.1). INRIA-Rocquencourt, 2000.
A. Bailey. The Machine-checked Literate Formalisation of Algebra in Type Theory. PhD thesis, University of Manchester, 1999.
G. Chen. Subtyping, Type Conversion and Transitivity Elimination. PhD thesis, University of Paris VII, 1998.
P. Callaghan and Z. Luo. An implementation of LF with coercive subtyping and universes. Journal of Automated Reasoning, 27(1):3–27, 2001.
P. C. Callaghan, Z. Luo, and J. Pang. Object languages in a type-theoretic meta-framework. Workshop of Proof Transformation and Presentation and Proof Complexities (PTP’01), 2001.
A. Jones, Z. Luo, and S. Soloviev. Some proof-theoretic and algorithmic aspects of coercive subtyping. Types for proofs and programs (eds, E. Gimenez and C. Paulin-Mohring), Proc. of the Inter. Conf. TYPES’96, LNCS 1512, 1998.
Z. Luo and P. Callaghan. Coercive subtyping and lexical semantics (extended abstract). LACL’98, 1998.
Y. Luo, Z. Luo, and S. Soloviev. Weak transitivity in coercive subtyping. In preparation, 2001.
Z. Luo and R. Pollack. LEGO Proof Development System: User’s Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992.
Z. Luo and S. Soloviev. Dependent coercions. The 8th Inter. Conf. on Category Theory and Computer Science (CTCS’99), Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science, 29, 1999.
Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.
Z. Luo. Coercive subtypingin type theory. Proc. of CSL’96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, 1997.
Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(1):105–130, 1999.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.
A. Saibi. Typingalg orithm in type theory with inheritance. Proc of POPL’97, 1997.
S. Soloviev and Z. Luo. Coercion completion and conservativity in coercive subtyping. To be published in Annals of Pure and Applied Logic, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Luo, Y., Luo, Z. (2001). Coherence and Transitivity in Coercive Subtyping. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_17
Download citation
DOI: https://doi.org/10.1007/3-540-45653-8_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42957-9
Online ISBN: 978-3-540-45653-7
eBook Packages: Springer Book Archive