{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:54Z","timestamp":1763468034312},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2010,6]]},"DOI":"10.1007\/s10990-011-9065-0","type":"journal-article","created":{"date-parts":[[2011,7,22]],"date-time":"2011-07-22T09:50:35Z","timestamp":1311328235000},"page":"145-166","source":"Crossref","is-referenced-by-count":3,"title":["A lean specification for GADTs: system F with first-class equality proofs"],"prefix":"10.1007","volume":"23","author":[{"given":"Arie","family":"Middelkoop","sequence":"first","affiliation":[]},{"given":"Atze","family":"Dijkstra","sequence":"additional","affiliation":[]},{"given":"S. Doaitse","family":"Swierstra","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,7,23]]},"reference":[{"key":"9065_CR1","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/581478.581494","volume-title":"ICFP","author":"A.I. Baars","year":"2002","unstructured":"Baars, A.I., Swierstra, S.D.: Typing dynamic typing. In: ICFP, pp. 157\u2013166 (2002)"},{"key":"9065_CR2","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/1481861.1481865","volume-title":"TLDI","author":"A.I. Baars","year":"2009","unstructured":"Baars, A.I., Swierstra, S.D., Viera, M.: Typed transformations of typed abstract syntax. In: Kennedy, A., Ahmed, A. (eds.) TLDI, pp. 15\u201326. ACM, New York (2009)"},{"key":"9065_CR3","unstructured":"Cheney, J., Hinze, R.: First-class phantom types. Tech. rep., Cornell University (2003)"},{"key":"9065_CR4","unstructured":"Dijkstra, A.: Stepping through Haskell. PhD thesis, Utrecht University, Department of Information and Computing Sciences (2005). http:\/\/www.cs.uu.nl\/wiki\/Ehc\/WebHome , papers\/dijkstra05phd.pdf"},{"key":"9065_CR5","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/1596638.1596650","volume-title":"Haskell","author":"A. Dijkstra","year":"2009","unstructured":"Dijkstra, A., Fokker, J., Swierstra, S.D.: The architecture of the Utrecht Haskell compiler. In: Weirich, S. (ed.) Haskell, pp. 93\u2013104. ACM, New York (2009)"},{"key":"9065_CR6","first-page":"165","volume-title":"AFP","author":"J. Jeuring","year":"2008","unstructured":"Jeuring, J., Leather, S., Magalh\u00e3es, J.P., Yakushev, AR: Libraries for generic programming in Haskell. In: AFP, pp. 165\u2013229 (2008)"},{"key":"9065_CR7","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/1708016.1708024","volume-title":"TLDI","author":"C. Lin","year":"2010","unstructured":"Lin, C., Sheard, T.: Pointwise generalized algebraic data types. In: Kennedy, A., Benton, N. (eds.) TLDI, pp. 51\u201362. ACM, New York (2010)"},{"key":"9065_CR8","first-page":"397","volume-title":"LICS","author":"M.J. Maher","year":"2005","unstructured":"Maher, M.J.: Herbrand constraint abduction. In: LICS, pp. 397\u2013406. IEEE Computer Society, Washington (2005)"},{"key":"9065_CR9","first-page":"65","volume-title":"TFP","author":"A. Middelkoop","year":"2008","unstructured":"Middelkoop, A., Dijkstra, A., Swierstra, S.D.: A leaner specification for generalized algebraic data types. In: TFP, vol. 9, pp. 65\u201380 (2008)"},{"issue":"3","key":"9065_CR10","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1017\/S0956796800000423","volume":"2","author":"T.\u00c6. Mogensen","year":"1992","unstructured":"Mogensen, T.\u00c6.: Efficient self-interpretations in lambda calculus. J. Funct. Program. 2(3), 345\u2013363 (1992)","journal-title":"J. Funct. Program."},{"key":"9065_CR11","unstructured":"Peyton\u00a0Jones, S.L., Washburn, G., Weirich, S.: Wobbly types: type inference for generalised algebraic data types. Tech. Rep. MS-CIS-05-26, University of Pennsylvania, Computer and Information Science Department, Levine Hall, 3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389 (2004)"},{"key":"9065_CR12","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1145\/1159803.1159811","volume-title":"ICFP","author":"S.L. Peyton\u00a0Jones","year":"2006","unstructured":"Peyton\u00a0Jones, S.L., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: ICFP, pp. 50\u201361 (2006)"},{"key":"9065_CR13","first-page":"232","volume-title":"POPL","author":"F. Pottier","year":"2006","unstructured":"Pottier, F., R\u00e9gis-Gianas, Y.: Stratified type inference for generalized algebraic data types. In: POPL, pp. 232\u2013244 (2006)"},{"key":"9065_CR14","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1145\/1596550.1596599","volume-title":"ICFP","author":"T. Schrijvers","year":"2009","unstructured":"Schrijvers, T., Jones, S.L.P., Sulzmann, M., Vytiniotis, D.: Complete and decidable type inference for GADTs. In: ICFP, pp. 341\u2013352 (2009)"},{"key":"9065_CR15","unstructured":"Stuckey, P.J., Sulzmann, M.: Type inference for guarded recursive data types. CoRR abs\/cs\/0507037 (2005)"},{"key":"9065_CR16","unstructured":"Sulzmann, M., Schrijvers, T., Stuckey, P.J.: Type inference for GADTs via Herbrand constraint abduction. Manuscript (2006)"},{"key":"9065_CR17","first-page":"47","volume-title":"FLOPS","author":"M. Sulzmann","year":"2006","unstructured":"Sulzmann, M., Wazny, J., Stuckey, P.J.: A framework for extended algebraic data types. In: FLOPS, pp. 47\u201364 (2006)"},{"key":"9065_CR18","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/1190315.1190324","volume-title":"TLDI","author":"M. Sulzmann","year":"2007","unstructured":"Sulzmann, M., Chakravarty, M.M.T., Peyton Jones, S.L., Donnelly, K.: System F with Type Equality Coercions. In: TLDI, pp. 53\u201366 (2007)"},{"issue":"1\u20132","key":"9065_CR19","doi-asserted-by":"crossref","first-page":"197","DOI":"10.3233\/FI-1996-281213","volume":"28","author":"P. Urzyczyn","year":"1996","unstructured":"Urzyczyn, P.: Positive recursive type assignment. Fundam. Inform. 28(1\u20132), 197\u2013209 (1996)","journal-title":"Fundam. Inform."},{"key":"9065_CR20","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1145\/1159803.1159838","volume-title":"ICFP","author":"D. Vytiniotis","year":"2006","unstructured":"Vytiniotis, D., Weirich, S., Peyton Jones, S.L.: Boxy types: inference for higher-rank types and impredicativity. In: Reppy, J.H., Lawall, J.L. (eds.) ICFP, pp. 251\u2013262. ACM, New York (2006)"},{"key":"9065_CR21","unstructured":"Wazny, J.R.: Type inference and type error diagnosis for Hindley\/Milner with extensions. PhD thesis, The university of Melbourne (2006)"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/s10990-011-9065-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,8]],"date-time":"2024-04-08T23:12:15Z","timestamp":1712617935000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-011-9065-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["9065"],"URL":"https:\/\/doi.org\/10.1007\/s10990-011-9065-0","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,6]]}}}