{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:42:30Z","timestamp":1770291750337,"version":"3.49.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319296036","type":"print"},{"value":"9783319296043","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29604-3_8","type":"book-chapter","created":{"date-parts":[[2016,2,20]],"date-time":"2016-02-20T07:53:12Z","timestamp":1455954792000},"page":"109-125","source":"Crossref","is-referenced-by-count":3,"title":["Executable Relational Specifications of Polymorphic Type Systems Using Prolog"],"prefix":"10.1007","author":[{"given":"Ki Yung","family":"Ahn","sequence":"first","affiliation":[]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,21]]},"reference":[{"key":"8_CR1","first-page":"54","volume-title":"Lecture Notes in Computer Science","author":"Andreas Abel","year":"2003","unstructured":"Abel, A., Matthes, R., Uustalu, T.: Generalized iteration and coiteration for higher-order nested datatypes. In: FoSSaCS 2003 (2003)"},{"key":"8_CR2","unstructured":"Ahn, K.Y.: The Nax language. Ph.D. thesis, Department of Computer Science, Portland State University, November 2014"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Ahn, K.Y., Sheard, T.: A hierarchy of Mendler-style recursion combinators. In: ICFP 2011. ACM (2011)","DOI":"10.1145\/2034773.2034807"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Ahn, K.Y., Sheard, T., Fiore, M., Pitts, A.M.: System Fi: a higher-order polymorphic lambda calculus with erasable term indices. In: TLCA 2013 (2013)","DOI":"10.1007\/978-3-642-38946-7_4"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Alves, S., Florido, M.: Type inference using Constraint Handling Rules. In: WFLP 2001, vol. 64 of Electronic Notes in TCS, pp. 56\u201372. Elsevier (2002)","DOI":"10.1016\/S1571-0661(04)80346-3"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-03013-0_2","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"D Ancona","year":"2009","unstructured":"Ancona, D., Lagorio, G.: Coinductive type systems for object-oriented languages. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 2\u201326. Springer, Heidelberg (2009)"},{"issue":"2","key":"8_CR7","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H Barendregt","year":"1991","unstructured":"Barendregt, H.: Introduction to generalized type systems. J. Funct. Program. 1(2), 125\u2013154 (1991)","journal-title":"J. Funct. Program."},{"key":"8_CR8","first-page":"52","volume-title":"Lecture Notes in Computer Science","author":"Richard Bird","year":"1998","unstructured":"Bird, R., Meertens, L.: Nested datatypes. In: MPC: 4th International Conference on Mathematics of Program Construction (1998)"},{"key":"8_CR9","unstructured":"Byrd, W.E.: Relational programming in miniKanren: techniques, applications,and implementations. Ph.D. thesis, Indiana University (2009)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-27775-0_19","volume-title":"Logic Programming","author":"J Cheney","year":"2004","unstructured":"Cheney, J., Urban, C.: \n                    \n                      \n                    \n                    $$\\alpha $$\n                  Prolog: A logic programming language with names, binding, and \n                    \n                      \n                    \n                    $$\\alpha $$\n                  -equivalence. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 269\u2013283. Springer, Heidelberg (2004)"},{"key":"8_CR11","unstructured":"Csorba, J., Zombori, Z., Szeredi, P.: Pros and cons of using CHR for type inference. In: CHR 2012, KU Leuven, Deptarment of CS, Tech-report CW 624 (2012)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-13346-1_11","volume-title":"Semantics of Data Types","author":"T Despeyroux","year":"1984","unstructured":"Despeyroux, T.: Executable specification of static semantics. In: MacQueen, D.B., Plotkin, G., Kahn, G. (eds.) Semantics of Data Types 1984. LNCS, vol. 173, pp. 215\u2013233. Springer, Heidelberg (1984)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-44659-1_9","volume-title":"Theorem Proving in Higher Order Logics","author":"C Dubois","year":"2000","unstructured":"Dubois, C.: Proving ML type soundness within Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 126\u2013144. Springer, Heidelberg (2000)"},{"key":"8_CR14","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5801.001.0001","volume-title":"The Reasoned Schemer","author":"DP Friedman","year":"2005","unstructured":"Friedman, D.P., Byrd, W.E., Kiselyov, O.: The Reasoned Schemer. MIT Press, Cambridge (2005). ISBN 978-0-262-56214-0"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Fu, P., Komendantskaya, E.: A type theoretic approach to structural resolution. In: Pre-Proceedings of LOPSTR 2015 (2015)","DOI":"10.1007\/978-3-319-27436-2_6"},{"key":"8_CR16","unstructured":"Gaster, B.R., Jones, M.P.: A polymorphic type system for extensible records and variants. Technical report (1996)"},{"key":"8_CR17","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII (1972)"},{"key":"8_CR18","unstructured":"Hemann, J., Friedman, D.P.: \n                    \n                      \n                    \n                    $$\\mu $$\n                  Kanren: A minimal functional core for relational programming. In: Scheme 2013 (2013)"},{"key":"8_CR19","unstructured":"Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Techincal Communications of ICLP (2015)"},{"key":"8_CR20","unstructured":"Jones, M.P.: Typing Haskell in Haskell. In: Haskell 1999, October 1999"},{"key":"8_CR21","unstructured":"Matthes, R.: Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. thesis, Ludwig-Maximilians University (1998)"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"1061","DOI":"10.1017\/S0956796803004957","volume":"13","author":"C McBride","year":"2003","unstructured":"McBride, C.: First-order unification by structural recursion. J. Func. Program. 13, 1061\u20131075 (2003). ISSN 1469\u20137653","journal-title":"J. Func. Program."},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"Automated Deduction - CADE-16","author":"DJ Mitchell","year":"1999","unstructured":"Mitchell, D.J., Nadathur, G.: System description: teyjus - a compiler and abstract machine based implementation of \n                    \n                      \n                    \n                    $$\\lambda $$\n                  prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287\u2013291. Springer, Heidelberg (1999)"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4","volume":"5","author":"M Odersky","year":"1999","unstructured":"Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theor. Pract. Object Syst. 5(1), 35\u201355 (1999). ISSN 1074\u20133227","journal-title":"Theor. Pract. Object Syst."},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0004-3702(80)90003-X","volume":"13","author":"FCN Pereira","year":"1980","unstructured":"Pereira, F.C.N., Warren, D.H.D.: Definite clause grammars for language analysis. Artif. Intell. 13, 231\u2013278 (1980)","journal-title":"Artif. Intell."},{"key":"8_CR26","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511794797","volume-title":"Artificial Intelligence - Foundations of Computational Agents","author":"D Poole","year":"2010","unstructured":"Poole, D., Mackworth, A.K.: Artificial Intelligence - Foundations of Computational Agents. Cambridge University Press, Cambridge (2010)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Russo, C.V., Vytiniotis, D.: Qml: explicit first-class polymorphism for ml. In: ML 2009, pp. 3\u201314. ACM, New York (2009)","DOI":"10.1145\/1596627.1596630"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/978-3-540-89982-2_59","volume-title":"Logic Programming","author":"T Schrijvers","year":"2008","unstructured":"Schrijvers, T., Costa, V.S., Wielemaker, J., Demoen, B.: Towards typed prolog. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 693\u2013697. Springer, Heidelberg (2008)"},{"issue":"4-5","key":"8_CR29","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1017\/S1471068413000331","volume":"13","author":"TOM SCHRIJVERS","year":"2013","unstructured":"Schrijvers, T., Demoen, B., Desouter, B., Wielemaker, J.: Delimited continuations for prolog. In: Proceedings of ICLP 2013 TPLP (2013)","journal-title":"Theory and Practice of Logic Programming"},{"key":"8_CR30","unstructured":"Scott, D.S.: A type-theoretic alternative to CUCH ISWIM OWHY. Manuscript (1969)"},{"key":"8_CR31","unstructured":"SWI-Prolog team. SWI-Prolog reference manual (section 4.2) (2005)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Urban, C., Nipkow, T.: Nominal verification of algorithm W. In: From Semantics to Computer Science, pp. 363\u2013382. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511770524.017"},{"key":"8_CR33","unstructured":"Vene, V.: Categorical Programming with Inductive and Coinductive Types. Ph.D. thesis, Department of Computer Science, University of Tartu, August 2000"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Yorgey, B.A., Weirich, S., Cretin, J., Peyton Jones, S., Vytiniotis, D., Magalh\u00e3es, J.P.: Giving Haskell a promotion. In: TLDI 2012. ACM (2012)","DOI":"10.1145\/2103786.2103795"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29604-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T10:57:19Z","timestamp":1559386639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29604-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296036","9783319296043"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29604-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}