{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:47:10Z","timestamp":1725670030892},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288685"},{"type":"electronic","value":"9783642288692"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_21","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T16:44:36Z","timestamp":1332434676000},"page":"417-435","source":"Crossref","is-referenced-by-count":0,"title":["Adding Equations to System F Types"],"prefix":"10.1007","author":[{"given":"Neelakantan R.","family":"Krishnaswami","sequence":"first","affiliation":[]},{"given":"Nick","family":"Benton","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L.: Formal parametric polymorphism. In: Principles of Programming Languages, pp. 157\u2013170 (1993)","DOI":"10.1145\/158511.158622"},{"key":"21_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-540-89439-1_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Abel","year":"2008","unstructured":"Abel, A.: Weak \u03b2\u03b7-Normalization and Normalization by Evaluation for System\u00a0F. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 497\u2013511. Springer, Heidelberg (2008)"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-02273-9_5","volume-title":"Typed Lambda Calculi and Applications","author":"R. Atkey","year":"2009","unstructured":"Atkey, R.: Syntax for Free: Representing Syntax with Binding Using Parametricity. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 35\u201349. Springer, Heidelberg (2009)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/BFb0014043","volume-title":"Typed Lambda Calculi and Applications","author":"R. Bellucci","year":"1995","unstructured":"Bellucci, R., Abadi, M., Curien, P.-L.: A Model for Formal Parametric Polymorphism: A PER Interpretation for System R. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 32\u201346. Springer, Heidelberg (1995)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Bernardy, J.-P., Jansson, P., Paterson, R.: Parametricity and dependent types. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, pp. 345\u2013356. ACM (2010)","DOI":"10.1145\/1863543.1863592"},{"issue":"1-3","key":"21_CR6","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1016\/j.tcs.2007.06.016","volume":"388","author":"L. Birkedal","year":"2007","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Petersen, R.L.: Domain-theoretical models of parametric polymorphism. Theoretical Computer Science\u00a0388(1-3), 152\u2013172 (2007)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"21_CR7","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1017\/S0960129510000162","volume":"20","author":"L. Birkedal","year":"2010","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Realisability semantics of parametric polymorphism, general references and recursive types. Mathematical Structures in Computer Science\u00a020(4), 655\u2013703 (2010)","journal-title":"Mathematical Structures in Computer Science"},{"key":"21_CR8","unstructured":"Cardelli, L., Leroy, X.: Abstract types and the dot notation. In: Broy, M., Jones, C.B. (eds.) Proceedings IFIP TC2 Working Conference on Programming Concepts and Methods, pp. 479\u2013504. North-Holland (1990)"},{"key":"21_CR9","unstructured":"Constable, R.L., Allen, S.F., Bromley, M., Cleaveland, R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the Nuprl proof development system. Prentice Hall (1986)"},{"issue":"2\/3","key":"21_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput.\u00a076(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Jones, S.P., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Reppy, J.H., Lawall, J.L. (eds.) Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, pp. 50\u201361. ACM (2006)","DOI":"10.1145\/1160074.1159811"},{"key":"21_CR12","unstructured":"Jones, S.P., Tolmach, A., Hoare, T.: Playing by the rules: rewriting as a practical optimisation technique in GHC. In: Haskell Workshop (2001)"},{"issue":"2","key":"21_CR13","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"Kahrs, S., Sannella, D., Tarlecki, A.: The definition of Extended ML: A gentle introduction. Theoretical Computer Science\u00a0173(2), 445\u2013484 (1997)","journal-title":"Theoretical Computer Science"},{"key":"21_CR14","unstructured":"Krishnaswami, N.R.: Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. PhD thesis, Carnegie Mellon University (2011)"},{"key":"21_CR15","first-page":"154","volume-title":"Functional Programming, Workshops in Computing","author":"S. Marlow","year":"1992","unstructured":"Marlow, S., Wadler, P.: Deforestation for higher-order functions. In: Launchbury, J., Sansom, P.M. (eds.) Functional Programming, Workshops in Computing, pp. 154\u2013165. Springer, Heidelberg (1992)"},{"key":"21_CR16","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"key":"21_CR17","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"J.C. Mitchell","year":"1988","unstructured":"Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst.\u00a010, 470\u2013502 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Neis, G., Dreyer, D., Rossberg, A.: Non-parametric parametricity. In: Hutton, G., Tolmach, A.P. (eds.) Proceeding of the 14th ACM SIGPLAN International Conference on Functional Programming, pp. 135\u2013148. ACM (2009)","DOI":"10.1145\/1596550.1596572"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Typed Lambda Calculi and Applications","author":"G.D. Plotkin","year":"1993","unstructured":"Plotkin, G.D., Abadi, M.: A Logic for Parametric Polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 361\u2013375. Springer, Heidelberg (1993)"},{"key":"21_CR20","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513\u2013523 (1983)"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. In: Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2010, ACM (2010)","DOI":"10.1145\/1708016.1708028"},{"issue":"1-3","key":"21_CR22","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/j.tcs.2006.12.042","volume":"375","author":"P. Wadler","year":"2007","unstructured":"Wadler, P.: The Girard-Reynolds isomorphism (second edition). Theoretical Computer Science\u00a0375(1-3), 201\u2013226 (2007)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,5]],"date-time":"2022-01-05T20:49:20Z","timestamp":1641415760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}