{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:08:03Z","timestamp":1774987683018,"version":"3.50.1"},"reference-count":42,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1991,10,1]],"date-time":"1991-10-01T00:00:00Z","timestamp":686275200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7960,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1991,10]]},"DOI":"10.1016\/0304-3975(90)90109-u","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T04:17:21Z","timestamp":1027657041000},"page":"137-159","source":"Crossref","is-referenced-by-count":24,"title":["Metacircularity in the polymorphic \u03bb-calculus"],"prefix":"10.1016","volume":"89","author":[{"given":"Frank","family":"Pfenning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(90)90109-U_BIB1","series-title":"Logic Programming","first-page":"153","article-title":"Amalgamating language and metalanguage in logic programming","author":"Bowen","year":"1982"},{"key":"10.1016\/0304-3975(90)90109-U_BIB2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","article-title":"Automatic synthesis of typed \u039b-programs on term algebras","volume":"39","author":"B\u00f6hm","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(90)90109-U_BIB3","series-title":"The Calculi of Lambda-Conversion","author":"Church","year":"1941"},{"key":"10.1016\/0304-3975(90)90109-U_BIB4","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(90)90109-U_BIB5","series-title":"OOPSLA '87: Proc. 1987 Conf. on Object-Oriented Programming Systems, Languages and Applications","first-page":"156","article-title":"Metaclasses are first class: the ObjVlisp model","author":"Cointe","year":"1987"},{"key":"10.1016\/0304-3975(90)90109-U_BIB6","series-title":"Symp. on Logic Computer Science","first-page":"227","article-title":"An analysis of Girard's paradox","author":"Coquand","year":"1986"},{"issue":"2\/3","key":"10.1016\/0304-3975(90)90109-U_BIB7","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The Calculus of Constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inform. and Comput."},{"key":"10.1016\/0304-3975(90)90109-U_BIB8","series-title":"Talk presented at the Workshop on Programming Logic","article-title":"Inductively defined types","author":"Coquand","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB9","series-title":"Documentation and User's Guide, Version 4.10","article-title":"Project Formel, The Calculus of Constructions","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB10","series-title":"Proc. 1984 ACM Symp. on Lisp and Functional Programming","first-page":"348","article-title":"Reification: reflection without metaphysics","author":"Friedman","year":"1984"},{"key":"10.1016\/0304-3975(90)90109-U_BIB11","series-title":"Logic and Computer Science","article-title":"On Girard's \u201cCandidats de R\u00e9ductibilit\u00e9","author":"Gallier","year":"1990"},{"key":"10.1016\/0304-3975(90)90109-U_BIB12","article-title":"Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dee l'arithm\u00e9tique d'ordre sup\u00e9rieur","volume":"VII","author":"Girard","year":"1972"},{"key":"10.1016\/0304-3975(90)90109-U_BIB13","series-title":"Proc. 2nd Scandinavian Logic Symp.","first-page":"63","article-title":"Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse, et son application a l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types","author":"Girard","year":"1971"},{"key":"10.1016\/0304-3975(90)90109-U_BIB14","article-title":"Proofs and Types","volume":"7","author":"Girard","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB15_1","doi-asserted-by":"crossref","unstructured":"R. Harper, F. Honsell and G. Plotkin, A framework for defining logics, J. ACM (to appear);","DOI":"10.1145\/138027.138060"},{"key":"10.1016\/0304-3975(90)90109-U_BIB15_2","series-title":"Symp. on Logic in Computer Science","first-page":"194","article-title":"A framework for defining logics","author":"Harper","year":"1987"},{"key":"10.1016\/0304-3975(90)90109-U_BIB16","series-title":"TAPSOFT '89, Proc. Internat. Joint Conf. on Theory and Practice in Software Development","first-page":"241","article-title":"Type checking, universe polymorphism, and typical ambiguity in the Calculus of Constructions","volume":"352","author":"Harper","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB17","series-title":"Ph.D. Thesis","article-title":"Automating Reasoning in an implementation of Constructive type theory","author":"Howe","year":"1987"},{"key":"10.1016\/0304-3975(90)90109-U_BIB18","series-title":"9th Internat. Conf. on Automated Deduction","first-page":"238","article-title":"Computational metatheory in Nuprl","volume":"310","author":"Howe","year":"1988"},{"key":"10.1016\/0304-3975(90)90109-U_BIB19","series-title":"4th Ann. Symp. on Logic in Computer Science","first-page":"386","article-title":"ECC, an extended Calculus of Constructions","author":"Luo","year":"1989"},{"issue":"4","key":"10.1016\/0304-3975(90)90109-U_BIB20","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","article-title":"Recursive functions of symbolic expressions and their computation by machine","volume":"3","author":"McCarthy","year":"1960","journal-title":"Comm. ACM"},{"issue":"2","key":"10.1016\/0304-3975(90)90109-U_BIB21_1","article-title":"The Standard ML core language","volume":"II","author":"Milner","year":"1985","journal-title":"Polymorphism"},{"key":"10.1016\/0304-3975(90)90109-U_BIB21_2","series-title":"Technical Report ECS-LFCS-86-2","article-title":"The Standard ML core language","author":"Milner","year":"1986"},{"key":"10.1016\/0304-3975(90)90109-U_BIB22","first-page":"810","article-title":"An overview of \u03bb Prolog","volume":"Volume 1","author":"Nadathur","year":"1988"},{"key":"10.1016\/0304-3975(90)90109-U_BIB23","article-title":"Extraction de programmes dans le Calcul des Constructions","volume":"VII","author":"Paulin-Mohring","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB24_1","series-title":"Proc. 1988 ACM Conf. on Lisp and Functional Programming","first-page":"153","article-title":"Partial polymorphic type inference and higher-order unification","author":"Pfenning","year":"1988"},{"key":"10.1016\/0304-3975(90)90109-U_BIB24_2","series-title":"Ergo-Report 88-036","first-page":"153","article-title":"Partial polymorphic type inference and higher-order unification","author":"Pfenning","year":"1988"},{"key":"10.1016\/0304-3975(90)90109-U_BIB25_1","series-title":"Proc. SIGPLAN '88 Symp. on Language Design and Implementation","first-page":"199","article-title":"Higher-order abstract syntax","author":"Pfenning","year":"1988"},{"key":"10.1016\/0304-3975(90)90109-U_BIB25_2","series-title":"Ergo Report 88-036","first-page":"199","article-title":"Higher-order abstract syntax","author":"Pfenning","year":"1988"},{"key":"10.1016\/0304-3975(90)90109-U_BIB26_1","series-title":"TAPSOFT '89, Proc. Internat. Joint Conf. on Theory and Practice in Software Development","first-page":"345","article-title":"LEAP: a language with eval and polymorphism","volume":"352","author":"Pfenning","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB26_2","series-title":"Ergo Report 88-065","first-page":"345","article-title":"LEAP: a language with eval and polymorphism","author":"Pfenning","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB27_1","series-title":"Proc. 5th Conf. on the Mathematical Foundations of Programming Semantics","article-title":"Inductively defined types in the Calculus of Constructions","author":"Pfenning","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB27_2","series-title":"Ergo Report 88-069","article-title":"Inductively defined types in the Calculus of Constructions","author":"Pfenning","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB28","series-title":"Technical Report CMU-CS-89-111","article-title":"Programming in higher-order typed lambda-calculi","author":"Pierce","year":"1989"},{"key":"10.1016\/0304-3975(90)90109-U_BIB29","author":"Pollack","year":"1988","journal-title":"The theory of LEGO"},{"key":"10.1016\/0304-3975(90)90109-U_BIB30","series-title":"Mathematical Foundations of Software Development","first-page":"97","article-title":"Three approaches to type structure","volume":"185","author":"Reynolds","year":"1985"},{"key":"10.1016\/0304-3975(90)90109-U_BIB31","series-title":"Proc. Coll. Programmation","first-page":"408","article-title":"Towards a theory of type structure","volume":"19","author":"Reynolds","year":"1974"},{"key":"10.1016\/0304-3975(90)90109-U_BIB32","first-page":"717","article-title":"Definitional interpreters for higher-order programming languages","author":"Reynolds","year":"1972"},{"key":"10.1016\/0304-3975(90)90109-U_BIB33","series-title":"Technical Report MIT-LCS-TR-272","article-title":"Reflection and semantics in a procedural language","author":"Smith","year":"1982"},{"key":"10.1016\/0304-3975(90)90109-U_BIB34","series-title":"Proc 11th ACM Symp. on Principles of Programming Languages","first-page":"23","article-title":"Reflection and semantics in Lisp","author":"Smith","year":"1984"},{"key":"10.1016\/0304-3975(90)90109-U_BIB35","series-title":"AI Memo 452","article-title":"The revised report on SCHEME\u2014a dialect of LISP","author":"Steele","year":"1978"},{"issue":"1","key":"10.1016\/0304-3975(90)90109-U_BIB36","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01806174","article-title":"The mystery of the tower revealed: a nonreflective description of the reflective tower","volume":"1","author":"Wand","year":"1988","journal-title":"Lisp Symbolic Comput."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759090109U?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759090109U?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T13:57:00Z","timestamp":1555077420000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759090109U"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,10]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,10]]}},"alternative-id":["030439759090109U"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(90)90109-u","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1991,10]]}}}