Abstract
Coercive subtyping offers a conceptually simple but powerful framework to understand subtyping and subset relationships in type theory. In this paper we study some of its proof-theoretic and computational properties.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
D. Aspinall and A. Compagnoni. Subtyping dependent types. Proc. of LICS96, 1996.
Anthony Bailey. Representing algebra in LEGO. Master's thesis, Department of Computer Science, University of Edinburgh, 1993.
A. Bailey. Lego with implicit coercions. 1996. Draft.
L. Cardelli. Type-checking dependent types and subtypes. Lecture Notes in Computer Science, 306, 1988.
L. Cardelli. Typeful programming. Lecture notes for the IFIP State of the Art Seminar on Formal Description of Programming Concepts, Rio de Janeiro, Brazil, 1989.
Th. Coquand. An algorithm for testing conversion in Type Theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.
H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.
G. Huet et al. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, February 1996.
Gérard Huet. The constructive engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. World Scientific Publishing, 1989. Commemorative Volume for Gift Siromoney.
Alex Jones. The formalization of linear algebra in LEGO: The decidable dependency theorem. Master's thesis, Department of Mathematics, University of Manchester, 1995.
Giuseppe Longo, Kathleen Milsted, and Sergei Soloviev. Coherence and transitivity of subtyping as entailment. To appear in Journal of Logic and Computation.
G. Longo, K. Milsted, and S. Soloviev. A logic of subtyping. In Proc. of LICS'95, 1995.
Zhaohui Luo and Robert Pollack. LEGO proof development system: User's manual. Technical Report LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992.
Z. Luo. Program specification and data refinement in type theory. Mathematical Structures in Computer Science, 3(3), 1993.
Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.
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, 1996.
Z Luo. Coercive suptyping. Draft submitted for publication, 1997.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory: An Introduction. Oxford University Press, 1990.
A. Saibi. Typing algorithm in type theory with inheritance. Proc. of POPL'97, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jones, A., Luo, Z., Soloviev, S. (1998). Some algorithmic and proof-theoretical aspects of coercive subtyping. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0097792
Download citation
DOI: https://doi.org/10.1007/BFb0097792
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65137-6
Online ISBN: 978-3-540-49562-8
eBook Packages: Springer Book Archive