Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Mathematical Foundations of Computer Science

MFCS 1997: Mathematical Foundations of Computer Science 1997 pp 189–198Cite as

Subtyping calculus of construction (extended abstract)

  • Contributed Papers
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1295))

Abstract

We present in this paper a subtyping extension of Calculus of Construction. We prove that this system has good meta-theoretical properties: transitivity elimination, subject reduction, strong normalization and decidability of subtyping. This work provides a theoretical foundation for adding subtyping to proof checkers like Coq, LEGO etc.

This work is supported by Programme PRA, Association Franco-Chinoise pour la Recherche Scientifique et Technique, and Bourse du Ministère des Affaires Etrangères du Gouvernement Français.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Aspinall and A. Compagnoni.Subtyping dependent types. In LICS'96.

    Google Scholar 

  2. A. Bailey. Lego with implicit coercions, 1996. draft.

    Google Scholar 

  3. H. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science. Oxford University Press, 1992.

    Google Scholar 

  4. G. Barthe. Inheritance in type theory, TYPES'95, 1995.

    Google Scholar 

  5. L. Cardelli. Typechecking dependent types and subtypes, December 1987.

    Google Scholar 

  6. P. L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and the type checking in F ≤ . MSCS, 2(1), 1992.

    Google Scholar 

  7. G. Chen. Dependent type system with subtyping. To appear in KIT Summer School and Workshop on Formal Models of Programming and their Applications, Beijing, 1997.

    Google Scholar 

  8. A. Compagnoni. Subtyping in F ωΛ is decidable. CSL'94.

    Google Scholar 

  9. G. Longo, K. Milsted, and S. Soloviev. A Logic of Subtyping. In LICS'95.

    Google Scholar 

  10. Z. Luo. Coercive subtyping in type theory. In CSL'96.

    Google Scholar 

  11. J.C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76:211–249, 1988.

    Article  Google Scholar 

  12. F. Pfenning. Refinement types for logical frameworks. In Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, May 1993.

    Google Scholar 

  13. A. Saibi. Typing algorithm in type theory with inheritance, 1996. in the 24th Annual SIGPLAN-SIGACT Symposium on principles of Programming Languages, Paris, France, January 15–17, 1997.

    Google Scholar 

  14. B. Pierce and M. Steffen. Higher-order subtyping. To appear in: Theoretical Computer Science, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Ecole Normale Supérieure,Laboratoire d'Informatique, 45, rue d'Ulm, 75230, Paris, France

    Gang Chen

Authors
  1. Gang Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Igor Prívara Peter Ružička

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chen, G. (1997). Subtyping calculus of construction (extended abstract). In: Prívara, I., Ružička, P. (eds) Mathematical Foundations of Computer Science 1997. MFCS 1997. Lecture Notes in Computer Science, vol 1295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0029962

Download citation

  • DOI: https://doi.org/10.1007/BFb0029962

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63437-9

  • Online ISBN: 978-3-540-69547-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation