Typing algorithm in type theory with inheritance

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Typing algorithm in type theory with inheritance

Full text

Pdf (667 KB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

Paris, France

Pages: 292 - 301

Year of Publication: 1997

ISBN:0-89791-853-3

Author

Amokrane Saïbi

INRIA Rocquencourt B.P. 105 - 78153 Le Chesnay Cedex, Université Pierre t Marie Curie - Paris

Sponsors

L'Ecole des Mines de Paris : L'Ecole des Mines de Paris
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Ctr Natl de la Recherche Sci :
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 25, Citation Count: 6

Additional Information:

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/263699.263742 What is a DOI?

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	P. Aczel. A notion of class }or theory development in algebra (in a predicative type theory). Presented at Workshop of Types for Proofs and Programs, Bastad, Sweden, June 1994.
	2	P. Aczel. Simple overloading for type theories. Privately circulated notes, 1994.
	3	Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
	4	H. P. Barendregt. Typed Lambda calculi, in Handbook of Logic in Computer Science, S. Abramsky et al. (Eds.), Oxford University Press, 117-309, 1992.
	5	G. Barthe. inheritance in type theory. Draft paper, 1995.
	6	G. Betarte. Classes and overloading in type theory with record types. Draft paper, 1995.
	7	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]
	8	C. Cornes, J. Courant, J-C. Filliatre, G. ttuet, P. Manoury, C. Munoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Sai#i, B. Werner. The Coq Proof Assistant Reference Manual, version 5.10. Rapport technique INRIA 0177, 1995.
	9	G. Huet. Extending the calculus of constructions with Type:Type. manuscrit non publiC, Avril 1987.
	10	Paul Bernard Jackson, Enhancing the NUPRL proof development system and applying it to computational abstract algebra, Cornell University, Ithaca, NY, 1996
	11	Z. Luo. Coercive Subtyping. Draft, 1995.
	12	Z. Luo et R. Pollack. LEGO proof development system: user's manual Technical Report ECS-LFCS- 92-211, LFCS, Computer Science Dept. University of Edinburg, Mai 1992.
	13	Christine Paulin-Mohring, Inductive Definitions in the system Coq - Rules and Properties, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.328-345, March 16-18, 1993
	14	C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Universit# Paris 7, January 1989.
	15	Paula Severi , Erik Poll, Pure Type Systems with Definitions, Proceedings of the Third International Symposium on Logical Foundations of Computer Science, p.316-328, July 11-14, 1994
	16	R. Pollack. The theory of LEGO: a proof checker for the Extended Calculus of Constructions. PhD thesis, university of Edinburgh, 1994.
	17	R. Pollack. Implicit Synatx. Informal Proceedings of First Workshop on Logical Frameworks, Antibes, Mai 1990.
	18	A. Sai#oi. Algdbre constructive en thdorie des types, Outils gdndriques pour la moddlisation et la ddmonstration, Application fi la thdorie des catdgories. PhD thesis, Paris VI university, forthcoming 1997.
	19	A. Sai"bi. Formalisation constructive de la thdorie des catdgories, in preparation, 1996.
	20	A. Tasistro. Extension of Martin-L6f theory of types with record types and subtyping. Draft paper, 1993.

CITED BY 6

	Herman Geuvers , Randy Pollack , Freek Wiedijk , Jan Zwanenburg, A constructive algebraic hierarchy in Coq, Journal of Symbolic Computation, v.34 n.4, p.271-286, October 2002
	Gang Chen, Coercive subtyping for the calculus of constructions, ACM SIGPLAN Notices, v.38 n.1, p.150-159, January 2003
	Zhaohui Luo , Yong Luo, Transitivity in coercive subtyping, Information and Computation, v.197 n.1/2, p.122-144, February 25, 2005/March 15, 2005
	Gilles Barthe, A computational view of implicit coercions in type theory, Mathematical Structures in Computer Science, v.15 n.5, p.839-874, October 2005
	Gilles Barthe , Venanzio Capretta , Olivier Pons, Setoids in type theory, Journal of Functional Programming, v.13 n.2, p.261-293, March 2003
	Zhaohui Luo, Coercions in a polymorphic type system, Mathematical Structures in Computer Science, v.18 n.4, p.729-751, August 2008