PER models of subtyping, recursive types and higher-order polymorphism

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

PER models of subtyping, recursive types and higher-order polymorphism

Full text

Pdf (1.21 MB)

Source

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

Albuquerque, New Mexico, United States

Pages: 316 - 327

Year of Publication: 1992

ISBN:0-89791-453-8

Authors

Kim Bruce
John C. Mitchell

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 28, Citation Count: 11

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/143165.143230 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.

	Ama91	Roberto M. Amadio, Recursion over realizability structures, Information and Computation, v.91 n.1, p.55-85, March 1991 [doi>10.1016/0890-5401(91)90074-C]
	AMSW91	S. Abramsky, J. Mitchell, A. Scedrov, and P. Wadler. Relators. Manuscript, 1991.
	AP90	M Abadi and G.D. Plotkin. A PER model of polymorphism and recursive types. In Proc. IEEE Syrup. on Logic in Computer Science, pages 355-365, 1990.
	Bar84	H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North- Holland, Amsterdam, 1984. Second edition.
	BL90	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]
	BMM90	Kim B. Bruce , Albert R. Meyer , John C. Mitchell, The semantics of second-order lambda calculus, Information and Computation, v.85 n.1, p.76-134, March 1990 [doi>10.1016/0890-5401(90)90044-I]
	BTCGS90	V. Breazu-Tannen , C. A. Gunter , A. Scedrov, Computing with coercions, Proceedings of the 1990 ACM conference on LISP and functional programming, p.44-60, June 27-29, 1990, Nice, France [doi>10.1145/91556.91590]
	BTCGS91	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]
	Car88	Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
	Car89	Felice Cardone, Relational Semantics for Recursive Types and Bounded Quantification, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.164-178, July 11-15, 1989
	Car91	L. Cardelli. Examples of type recursion. Personal communication, 1991.
	CCH+89	Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99392]
	CCH91	P. Canning, W. Cook, and W. Hill. Examples of type recursion. Personal communication, 1991.
	CHC90	William R. Cook , Walter Hill , Peter S. Canning, Inheritance is not subtyping, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.125-135, December 1989, San Francisco, California, United States [doi>10.1145/96709.96721]
	CL90	L. Cardelli and G. Longo. A semantic basis for Quest. Technical Report 55, DEC Systems Research Center, 1990. To appear in J. Functional Programming.
	CM91	Luca Cardelli , John C. Mitchell, Operations on Records, Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics, p.22-52, March 29-April 01, 1989
	Coo89	W.R. Cook. A proposal for making Eiffel type-safe. In European Conf. on Objec#Oriented Programming, pages 57- 72, 1989.
	Cop85	Mario Coppo, A Completeness Theorem for Recursively Defined Types, Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.120-129, July 15-19, 1985
	CW85	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]
	FRMS90	P. Freyd, G. Rosolini, P. Mulry, and D.S. Scott. Extens ional P EP~'s. in Proc. IEEE Symp. on Logic in Computer Science, pages 346-354. IEEE, 1990.
	Gir72	J.-Y. Girard. Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur. These D'Etat, Universite Paris VII, 1972.
	GS90	C. A. Gunter , D. S. Scott, Semantic domains, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	Hen89	Friedrich Henglein , Robert Paige, Polymorphic type inference and semiunification, 1989
	KTU89	A. Kfoury , J. Tiuryn , P. Urzyczyn, Computational consequences and partial solutions of a generalized unification problem, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.98-105, June 1989, Pacific Grove, California, United States
	LS86	J. Lambek , P. J. Scott, Introduction to higher order categorical logic, Cambridge University Press, New York, NY, 1986
	Mit86	John C. Mitchell, A type-inference approach to reduction properties and semantics of polymorphic expressions (summary), Proceedings of the 1986 ACM conference on LISP and functional programming, p.308-319, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319872]
	Mit90a	John C. Mitchell, Toward a typed foundation for method specialization and inheritance, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-124, December 1989, San Francisco, California, United States [doi>10.1145/96709.96719]
	Mit90b	John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	Myc84	Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
	SP82	M. Smyth and G.D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM J. Computing, 11:761-783, 1982.
	Tro73	A.S. Troelstra. Maihema~icat I~vee~igation of Intuitionistic Arithmetic and Analysis. Springer LNM 344, Berlin, 1973.

CITED BY 11

	Martín Abadi , Luca Cardelli, On subtyping and matching, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.4, p.401-423, July 1996
	Kim B. Bruce, Safe type checking in a statically-typed object-oriented programming language, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.285-298, March 1993, Charleston, South Carolina, United States
	Adriana Compagnoni , Healfdene Goguen, Typed operational semantics for higher-order subtyping, Information and Computation, v.184 n.2, p.242-297, August 01, 2003
	Kim B. Bruce , Jon Crabtree , Thomas P. Murtagh , Robert van Gent , Allyn Dimock , Robert Muller, Safe and decidable type checking in an object-oriented language, ACM SIGPLAN Notices, v.28 n.10, p.29-46, Oct. 1, 1993
	Benjamin C. Pierce , David N. Turner, Object-oriented programming without recursive types, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.299-312, March 1993, Charleston, South Carolina, United States
	Giuseppe Castagna , Benjamin C. Pierce, Decidable bounded quantification, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.151-162, January 16-19, 1994, Portland, Oregon, United States
	Kim B. Bruce , Angela Schuett , Robert van Gent , Adrian Fiech, PolyTOIL: A type-safe polymorphic object-oriented language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.2, p.225-290, March 2003
	Adriana Compagnoni, Higher-order subtyping and its decidability, Information and Computation, v.191 n.1, p.41-103, May 25, 2004
	Adrian Fiech , David A. Schmidt, Polymorphic lambda calculus and subtyping, Theoretical Computer Science, v.278 n.1-2, p.111-140, May 6, 2002
	Jerome Vouillon , Paul-André Melliès, Semantic types: a fresh look at the ideal model for types, ACM SIGPLAN Notices, v.39 n.1, p.52-63, January 2004
	Benjamin C. Pierce, Intersection types and bounded polymorphism, Mathematical Structures in Computer Science, v.7 n.2, p.129-193, April 1997