{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:22:51Z","timestamp":1725456171766},"publisher-location":"Berlin\/Heidelberg","reference-count":34,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354017611X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0014987","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T01:02:53Z","timestamp":1132707773000},"page":"291-307","source":"Crossref","is-referenced-by-count":1,"title":["Extensional models for polymorphism"],"prefix":"10.1007","author":[{"given":"Val","family":"Breazu-Tannen","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","volume-title":"The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics","author":"H. P. Barendregt","year":"1984","unstructured":"H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, second edition, 1984.","edition":"second edition"},{"key":"19_CR2","unstructured":"V. Breazu-Tannen. Ph.D. thesis, MIT. Expected Feb.1987."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen and A. R. Meyer. Computable values can be classical. In Proceedings of the 14th Symposium on Principles of Programming Languages, ACM, 1987. To appear.","DOI":"10.1145\/41625.41646"},{"key":"19_CR4","unstructured":"V. Breazu-Tannen. Communication in the Types electronic forum (xx.lcs.mit.edu), July 29th. 1986. Unpublished."},{"key":"19_CR5","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/3-540-13346-1_6","volume-title":"Semantics of Data Types","author":"K. B. Bruce","year":"1984","unstructured":"K. B. Bruce and A. R. Meyer. The semantics of second order polymorphic lambda calculus. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, pages 131\u2013144, Springer-Verlag, Berlin, June 1984."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"R. M. Burstall, D.B. MacQueen, and D.T. Sanella. Hope: an experimental applicative language. In LISP Conference, pages 136\u2013143, Stanford University Computer Science Department, 1980.","DOI":"10.1145\/800087.802799"},{"issue":"4","key":"19_CR7","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. Computing Surveys, 17(4):471\u2013522, 1985.","journal-title":"Computing Surveys"},{"key":"19_CR8","volume-title":"Combinators and functional programming languages, Proceedings of the 13th Summer School of the LITP","author":"L. Cardelli","year":"1985","unstructured":"L. Cardelli. Amber. In Combinators and functional programming languages, Proceedings of the 13th Summer School of the LITP, Le Val D'Ajol, Vosges, France, May 1985."},{"key":"19_CR9","unstructured":"T. Coquand. Communication in the Types electronic forum (xx.lcs.mit.edu), April 14th. 1986. Unpublished."},{"key":"19_CR10","series-title":"Tech. Rep.","volume-title":"Ponder and its type system","author":"J. Fairbairn","year":"1982","unstructured":"J. Fairbairn. Ponder and its type system. Tech. Rep. 31, Computer Laboratory, Univ. of Cambridge, Cambridge, England, November 1982."},{"issue":"1","key":"19_CR11","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S. Fortune","year":"1983","unstructured":"S. Fortune, D. Leivant, and M. O'Donnell. The expressiveness of simple and second-order type structures. Journal of the ACM, 30(1):151\u2013185, January 1983.","journal-title":"Journal of the ACM"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"R. O. Gandy. On the axiom of extensionality\u2014Part I. Journal of Symbolic Logic, 21, 1956.","DOI":"10.2307\/2268484"},{"key":"19_CR13","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure. Ph.D. thesis, Universit\u00e9 Paris VII, 1972."},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. J. Gordon","year":"1979","unstructured":"M. J. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1979."},{"key":"19_CR15","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19800261902","volume":"26","author":"R. Hindley","year":"1980","unstructured":"R. Hindley and G. Longo. Lambda-calculus models and extensionality. Zeitschrift f\u00fcr Mathematische Logic und Grundlagen der Mathematik, 26:289\u2013310, 1980.","journal-title":"Zeitschrift f\u00fcr Mathematische Logic und Grundlagen der Mathematik"},{"key":"19_CR16","volume-title":"Combinatory reduction systems. Tract 129","author":"J. W. Klop","year":"1980","unstructured":"J. W. Klop. Combinatory reduction systems. Tract 129, Mathematical Center, Amsterdam, 1980."},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"D. Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In 24th Symposium on Foundations of Computer Science, pages 460\u2013469, IEEE, 1983.","DOI":"10.1109\/SFCS.1983.50"},{"key":"19_CR18","series-title":"Tech. Rep.","volume-title":"Poly manual.","author":"D. C. J. Matthews","year":"1985","unstructured":"D. C. J. Matthews. Poly manual. Tech. Rep. 63, Computer Laboratory, Univ. of Cambridge, Cambridge, England, 1985."},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"A. R. Meyer, J. C. Mitchell, E. Moggi, and R. Statman. Empty types in polymorphic \u03bb-calculus. In Proceedings of the 14th Symposium on Principles of Programming Languages, ACM, 1987. To appear.","DOI":"10.1145\/41625.41648"},{"issue":"1","key":"19_CR20","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A. R. Meyer","year":"1982","unstructured":"Albert R. Meyer. What is a model of the lambda calculus? Information and Control, 52(1):87\u2013122, January 1982.","journal-title":"Information and Control"},{"key":"19_CR21","unstructured":"A. R. Meyer. Communication in the Types electronic forum (xx.lcs.mit.edu), February 7th. 1986. Unpublished."},{"key":"19_CR22","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-15648-8_18","volume-title":"Logics of Programs","author":"J. C. Mitchell","year":"1985","unstructured":"J. C. Mitchell and A.R. Meyer. Second-order logic relations (extended abstract). In R. Parikh, editor, Logics of Programs, pages 225\u2013236, Springer-Verlag, Berlin, June 1985."},{"key":"19_CR23","unstructured":"J. C. Mitchell. Personal communication, August. 1986. Unpublished."},{"key":"19_CR24","first-page":"308","volume-title":"LISP Conference","author":"J. C. Mitchell","year":"1986","unstructured":"J. C. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions. In LISP Conference, pages 308\u2013319, ACM, New York, August 1986."},{"key":"19_CR25","unstructured":"E. Moggi. Communication in the Types electronic forum (xx.lcs.mit.edu), February 10th. 1986. Unpublished."},{"key":"19_CR26","unstructured":"E. Moggi. Communication in the Types electronic forum (xx.lcs.mit.edu), July 23rd. 1986. Unpublished."},{"key":"19_CR27","unstructured":"R. S. Nikhil. An incremental, strongly typed database query language. Ph.D. thesis, Univ. of Pennsylvania, Philadelphia, August 1984. Available as tech. rep. MS-CIS-85-02."},{"key":"19_CR28","volume-title":"TAPSOFT advanced seminar on the role of semantics in software development","author":"J. C. Reynolds","year":"1985","unstructured":"J. C. Reynolds. Three approaches to type structure. In TAPSOFT advanced seminar on the role of semantics in software development, Springer-Verlag, Berlin, 1985."},{"key":"19_CR29","unstructured":"A. Scedrov. Semantical methods for polymorphism. 1986. Unpublished manuscript, Univ. of Pennsylvania, July 1986."},{"key":"19_CR30","first-page":"511","volume-title":"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism","author":"R. Statman","year":"1980","unstructured":"R. Statman. On the existence of closed terms in the typed \u03bb-calculus. In J. P. Seldin and R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 511\u2013534, Academic Press, New York, 1980."},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"R. Statman. Number theoretic functions computable by polymorphic programs. In 22nd Symposium on Foundations of Computer Science, pages 279\u2013282, IEEE, 1981.","DOI":"10.1109\/SFCS.1981.24"},{"key":"19_CR32","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF02023009","volume":"23","author":"R. Statman","year":"1983","unstructured":"R. Statman. \u03bb-definable functionals and \u03b2\n                \u03b7 conversion. Arch. math. Logik, 23:21\u201326, 1983.","journal-title":"Arch. math. Logik"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra (ed.). Metamathematical investigation of intuititionistic arithmetic and analysis. Volume 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.","DOI":"10.1007\/BFb0066739"},{"key":"19_CR34","first-page":"1","volume-title":"Functional programming languages and computer architecture","author":"D. A. Turner","year":"1985","unstructured":"D. A. Turner. Miranda: a non-strict functional language with polymorphic types. In J.-P. Jouannaud, editor, Functional programming languages and computer architecture, pages 1\u201316, Springer-Verlag, Berlin, September 1985."}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '87"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014987.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T10:09:00Z","timestamp":1607335740000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354017611X"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/bfb0014987","relation":{},"subject":[]}}