{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:22:51Z","timestamp":1720624971001},"reference-count":21,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2006,11,1]],"date-time":"2006-11-01T00:00:00Z","timestamp":1162339200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":2462,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2006,11]]},"DOI":"10.1016\/j.entcs.2006.05.041","type":"journal-article","created":{"date-parts":[[2006,11,14]],"date-time":"2006-11-14T15:46:46Z","timestamp":1163519206000},"page":"121-132","source":"Crossref","is-referenced-by-count":8,"special_numbering":"C","title":["Formalizing Type Operations Using the \u201cImage\u201d Type Constructor"],"prefix":"10.1016","volume":"165","author":[{"given":"Aleksey","family":"Nogin","sequence":"first","affiliation":[]},{"given":"Alexei","family":"Kopylov","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2006.05.041_bib001","unstructured":"Allen, S.F., A Non-type-theoretic Definition of Martin-L\u00f6f's Types, in: D. Gries, editor, Proceedings of the 2nd IEEE Symposium on Logic in Computer Science (1987), pp. 215\u2013224"},{"key":"10.1016\/j.entcs.2006.05.041_bib002","unstructured":"Allen, S.F., \u201cA Non-Type-Theoretic Semantics for Type-Theoretic Language,\u201d Ph.D. thesis, Cornell University (1987)"},{"key":"10.1016\/j.entcs.2006.05.041_bib003","unstructured":"Backhouse, R., On the meaning and construction of the rules in Martin-L\u00f6f's theory of types, in: A. Avron, editor, Workshop on General Logic, Edinburgh, February 1987, number 88-52 in ECS-LFCS (1988)"},{"key":"10.1016\/j.entcs.2006.05.041_bib004","first-page":"205","article-title":"Do-it-yourself type theory (part II)","volume":"35","author":"Backhouse","year":"1988","journal-title":"EATCS Bulletin"},{"key":"10.1016\/j.entcs.2006.05.041_bib005","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/BF01887198","article-title":"Do-it-yourself type theory","volume":"1","author":"Backhouse","year":"1989","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/j.entcs.2006.05.041_bib006","series-title":"Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics","volume":"2410","year":"2002"},{"key":"10.1016\/j.entcs.2006.05.041_bib007","series-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/j.entcs.2006.05.041_bib008","series-title":"LPAR '94: Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning","first-page":"159","article-title":"Higher-order abstract syntax with induction in Coq","volume":"822","author":"Despeyroux","year":"1994"},{"key":"10.1016\/j.entcs.2006.05.041_bib009","series-title":"Proceedings of the International Conference on Typed Lambda Calculus and its Applications","first-page":"147","article-title":"Primitive recursion for higher\u2013order abstract syntax","volume":"1210","author":"Despeyroux","year":"1997"},{"key":"10.1016\/j.entcs.2006.05.041_bib010","series-title":"Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics","first-page":"287","article-title":"MetaPRL modular logical environment","volume":"2758","author":"Hickey","year":"2003"},{"key":"10.1016\/j.entcs.2006.05.041_bib011","unstructured":"Hickey, J.J., \u201cThe MetaPRL Logical Programming Environment,\u201d Ph.D. thesis, Cornell University, Ithaca, NY (2001). URL http:\/\/www.nuprl.org\/documents\/Hickey\/Hickeythesis.html"},{"key":"10.1016\/j.entcs.2006.05.041_bib012","author":"Hickey"},{"key":"10.1016\/j.entcs.2006.05.041_bib013","author":"Hickey"},{"key":"10.1016\/j.entcs.2006.05.041_bib014","doi-asserted-by":"crossref","unstructured":"Howe, D.J., Equality in lazy computation systems, in: Proceedings of the 4th IEEE Symposium on Logic in Computer Science (1989), pp. 198\u2013203","DOI":"10.1109\/LICS.1989.39174"},{"key":"10.1016\/j.entcs.2006.05.041_bib015","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P., Constructive mathematics and computer programming, in: Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science (1982), pp. 153\u2013175","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"10.1016\/j.entcs.2006.05.041_bib016","article-title":"Intuitionistic Type Theory","volume":"Number 1","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/j.entcs.2006.05.041_bib017","doi-asserted-by":"crossref","unstructured":"Nogin, A., Quotient types: A modular approach, in: Carre\u00f1o et al. [6], pp. 263\u2013280. URL http:\/\/nogin.org\/papers\/quotients.html","DOI":"10.1007\/3-540-45685-6_18"},{"key":"10.1016\/j.entcs.2006.05.041_bib018","doi-asserted-by":"crossref","unstructured":"Nogin, A. and J. Hickey, Sequent schema for derived rules, in: Carre\u00f1o et al. [6], pp. 281\u2013297. URL http:\/\/nogin.org\/papers\/derived_rules.html","DOI":"10.1007\/3-540-45685-6_19"},{"key":"10.1016\/j.entcs.2006.05.041_bib019","doi-asserted-by":"crossref","unstructured":"Nogin, A., A. Kopylov, X. Yu and J. Hickey, A computational approach to reflective meta-reasoning about languages with bindings, in: MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding (2005), pp. 2\u201312, an extended version is available as California Institute of Technology technical report CaltechCSTR:2005.003","DOI":"10.1145\/1088454.1088456"},{"key":"10.1016\/j.entcs.2006.05.041_bib020","unstructured":"Pierce, B.C., Programming with intersection types, union types, and polymorphism, Technical Report CMU-CS-91-106, Carnegie Mellon University (1991)"},{"key":"10.1016\/j.entcs.2006.05.041_bib021","article-title":"Metamathematical Investigation of Intuitionistic Mathematics","volume":"344","author":"Troelstra","year":"1973"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066106005184?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066106005184?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T10:05:08Z","timestamp":1555927508000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066106005184"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":21,"alternative-id":["S1571066106005184"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2006.05.041","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2006,11]]}}}