Coercive subtyping for the calculus of constructions

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Coercive subtyping for the calculus of constructions

Full text

Pdf (219 KB)

Source

ACM SIGPLAN Notices archive
Volume 38 , Issue 1 (January 2003) table of contents

Pages: 150 - 159

Year of Publication: 2003

ISSN:0362-1340

Also published in ...

Author

Gang Chen

Boston University, Boston, MA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 32, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/640128.604145 What is a DOI?

ABSTRACT

We present a coercive subtyping system for the calculus of constructions. The proposed system λC^COover≤ is obtained essentially by adding coercions and η-conversion to λC≤[10], which is a subtyping extension to the calculus of constructions without coercions. Following [17, 18], the coercive subtyping c : A η B is understood as a special case of typing in arrow type c : A → B such that the term c behaves like an identity function. We prove that, with respect to this semantic interpretation, the proposed coercive subtyping system is sound and complete, and that this completeness leads to transitivity elimination (transitivity rule is admissible). In addition, we establish the equivalence between λC^COover≤ and CCßη, this fact implies that λC^COover≤ has confluence, subject reduction and strong normalization. We propose a formalization of coercion inference problem and present a sound and complete coercion inference algorithm.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	David Aspinall , Adriana Compagnoni, Subtyping Dependent Types, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.86, July 27-30, 1996
	2	A. Bailey. Lego with implicit coercions, 1996. draft.
	3	Gilles Barthe, Implicit Coercions in Type Systems, Selected papers from the International Workshop on Types for Proofs and Programs, p.1-15, June 05-08, 1995
	4	Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
	5	Kim B. Bruce , Giuseppe Longo, A modest model of records, inheritance, and unbounded quantification, Information and Computation, v.87 n.1-2, p.196-240, July/August 1990 [doi>10.1016/0890-5401(90)90062-M]
	6	L. Cardelli, Typechecking dependent types and subtypes, Lecture notes in computer science on Foundations of logic and functional programming, p.45-57, June 1988, Trento, Italy
	7	Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
	8	Giuseppe Castagna, Object-oriented programming: a unified foundation, Birkhauser Boston Inc., Cambridge, MA, 1997
	9	G. Chen. Dependent type system with subtyping. Technical Report LIENS-96-27, Laboratoire d'Informatique, Ecole Normale Supérieure - Paris, 12 1996. Revised version in Journal of Computer Science and Technology, vol. 14, no. 1 (1999).
	10	Gang Chen, Subtyping Calculus of Construction (Extended Abstract), Proceedings of the 22nd International Symposium on Mathematical Foundations of Computer Science, p.189-198, August 25-29, 1997
	11	G. Chen. Subtyping, type conversions and elimination of transitivity. PhD thesis, Université Paris 7, December 1998.
	12	A. B. Compagnoni. Subtyping in Fωover∧ is decidable. Technical Report ECS-LFCS-94-281, LFCS University of Edinburgh, January 1994. and in CSL'94.
	13	P.-L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and the type checking in F≤. Mathematical Structures in Computer Science, 2(1):55--91, 1992.
	14	H. Geuvers. Logics and Type Systems. PhD thesis, University of Nijmegen, Netherlands, 1993.
	15	A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. In Workshop on Subtyping, Inheritance and Modular Development of Proofs, September 1997. Durham, U.K.
	16	M. Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, CMU, May 1997. CMU-CS-97-122.
	17	G. Loop , K. Milsted , S. Soloviev, A logic of subtyping, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.292, June 26-29, 1995
	18	G. Longo, K. Milsted, and S. Soloviev. Coherence and transitivity of subtyping as entailment, 1998. Journal of Logic and Computation., vol. 10: 4, pp. 493--526, August 2000.
	19	Yong Luo , Zhaohui Luo, Coherence and Transitivity in Coercive Subtyping, Proceedings of the Artificial Intelligence on Logic for Programming, p.249-265, December 03-07, 2001
	20	Zhaohui Luo, Coercive Subtyping in Type Theory, Selected Papers from the10th International Workshop on Computer Science Logic, p.276-296, September 21-27, 1996
	21	Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(97--13), 1997.
	22	John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
	23	Benjamin Pierce , Martin Steffen, Higher-order subtyping, Theoretical Computer Science, v.176 n.1-2, p.235-282, April 20, 1997 [doi>10.1016/S0304-3975(96)00096-5]
	24	Amokrane Saïbi, Typing algorithm in type theory with inheritance, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.292-301, January 15-17, 1997, Paris, France [doi>10.1145/263699.263742]
	25	S. Soloviev and Z. Luo. Coercion completion and conservativity in coercive subtyping. Annalsof Pure and Applied Logic, 113(1-3):297--322, 2002.