{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:07Z","timestamp":1775790787799,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662488980","type":"print"},{"value":"9783662488997","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_32","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"460-468","source":"Crossref","is-referenced-by-count":26,"title":["ELPI: Fast, Embeddable, $$\\lambda $$ Prolog Interpreter"],"prefix":"10.1007","author":[{"given":"Cvetan","family":"Dunchev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ferruccio","family":"Guidi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 84\u201398. Springer, Heidelberg (2009)"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C. (eds.) Selected Papers on Automath, pp. 375\u2013388. North-Holland, Amsterdam (1994)","DOI":"10.1016\/S0049-237X(08)70216-7"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O\u2019Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy, Sandrine, Paulin-Mohring, Christine, Pichardie, David (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013)"},{"issue":"4","key":"32_CR4","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1017\/S0956796813000051","volume":"23","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. J. Funct. Program. 23(4), 357\u2013401 (2013)","journal-title":"J. Funct. Program."},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Guidi, F.: The formal system \n                    \n                      \n                    \n                    $$\\lambda \\delta $$\n                  . In: ToCL, vol. 11(1), pp. 1\u201337, November 2009","DOI":"10.1145\/1614431.1614436"},{"key":"32_CR6","unstructured":"Guidi, F.: Verified representations of Landau\u2019s \u201cGrundlagen\u201d in \n                    \n                      \n                    \n                    $$\\lambda \\delta $$\n                   and in the calculus of constructions (2015). \n                    http:\/\/lambdadelta.info\/\n                    \n                  , Submitted to JFR"},{"issue":"2","key":"32_CR7","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10817-004-6885-1","volume":"33","author":"C Liang","year":"2004","unstructured":"Liang, C., Nadathur, G., Qi, X.: Choices in representation and reduction strategies for lambda terms in intensional contexts. JAR 33(2), 89\u2013132 (2004)","journal-title":"JAR"},{"key":"32_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Comput. 1, 253\u2013281 (1991)","journal-title":"J. Logic Comput."},{"key":"32_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order Logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)"},{"key":"32_CR10","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":"G Nadathur","year":"1999","unstructured":"Nadathur, G., Mitchell, D.J.: System description: Teyjus - a compiler and abstract machine based implementation of \n                    \n                      \n                    \n                    $$\\lambda $$\n                   prolog. In: Ganzinger, Harald (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287\u2013291. Springer, Heidelberg (1999)"},{"key":"32_CR11","unstructured":"Ridoux, O.: \n                    \n                      \n                    \n                    $$\\lambda $$\n                  -Prolog de A a Z... ou presque. Habilitation \u00e0 diriger des recherches, Universit\u00e9 de Rennes 1 (1998)"},{"key":"32_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"32_CR13","unstructured":"van Benthem Jutting, L.S.: Checking Landau\u2019s \u201cGrundlagen\u201d in the Automath system. In: Mathematical Centre Tracts, vol. 83. Mathematisch Centrum (1979)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:31:01Z","timestamp":1559331061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}