{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T21:03:47Z","timestamp":1768683827418,"version":"3.49.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,3,2]],"date-time":"2011-03-02T00:00:00Z","timestamp":1299024000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10817-011-9219-0","type":"journal-article","created":{"date-parts":[[2011,3,2]],"date-time":"2011-03-02T00:05:41Z","timestamp":1299024341000},"page":"141-159","source":"Crossref","is-referenced-by-count":56,"title":["Strongly Typed Term Representations in Coq"],"prefix":"10.1007","volume":"49","author":[{"given":"Nick","family":"Benton","sequence":"first","affiliation":[]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[]},{"given":"Andrew J.","family":"Kennedy","sequence":"additional","affiliation":[]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,3,2]]},"reference":[{"key":"9219_CR1","doi-asserted-by":"crossref","unstructured":"Adams, R.: Formalized metatheory with terms represented by an indexed family of types. In: Types for Proofs and Programs. Lecture Notes in Computer Science, vol. 3839, pp. 1\u201316. Springer (2006)","DOI":"10.1007\/11617990_1"},{"key":"9219_CR2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Computer Science Logic, 13th International Workshop (CSL\u201999). Lecture Notes in Computer Science, vol. 1683, pp. 453\u2013468. Springer (1999)","DOI":"10.1007\/3-540-48168-0_32"},{"key":"9219_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N., Hur, C.K.: Biorthogonality, step-indexing and compiler correctness. In: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201909), pp. 97\u2013108. ACM (2009)","DOI":"10.1145\/1596550.1596567"},{"key":"9219_CR4","unstructured":"Benton, N., Hur, C.K.: Realizability and compositional compiler correctness for a polymorphic language. Tech. Rep. MSR-TR-2010-62, Microsoft Research (2010)"},{"key":"9219_CR5","doi-asserted-by":"crossref","unstructured":"Benton, N., Kennedy, A.J., Varming, C.: Some domain theory and denotational semantics in Coq. In: Theorem Proving in Higher Order Logics, 22nd International Conference (TPHOLs\u201909). Lecture Notes in Computer Science, vol. 5674, pp. 115\u2013130. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_10"},{"key":"9219_CR6","doi-asserted-by":"crossref","unstructured":"Bird, R., Meertens, L.: Nested datatypes. In: Proceedings of the 4th International Conference on Mathematics of Program Construction (MPC\u201998). Lecture Notes in Computer Science, vol. 1422, pp. 52\u201367. Springer (1998)","DOI":"10.1007\/BFb0054285"},{"key":"9219_CR7","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1017\/S0956796899003366","volume":"9","author":"R Bird","year":"1999","unstructured":"Bird, R., Paterson, R.: de Bruijn notation as a nested datatype. J. Funct. Program. 9, 77\u201391 (1999)","journal-title":"J. Funct. Program."},{"key":"9219_CR8","doi-asserted-by":"crossref","unstructured":"Brady, E., Hammond, K.: A verified staged interpreter is a verified compiler. In: Proceedings of the 5th International Conference on Generative Programming and Component Engineering (GPCE\u201906), pp. 111\u2013120. ACM (2006)","DOI":"10.1145\/1173706.1173724"},{"key":"9219_CR9","doi-asserted-by":"crossref","unstructured":"Chapman, J.: Type theory should eat itself. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP\u201908). Electr. Notes Theor. Comput. Sci., vol. 228, pp. 21\u201336. Elsevier (2009)","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"9219_CR10","unstructured":"Cheney, J., Hinze, R.: First-class phantom types. Tech. Rep. TR2003-1901, Cornell University (2003)"},{"key":"9219_CR11","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201908), pp. 143\u2013156. ACM (2008)","DOI":"10.1145\/1411204.1411226"},{"key":"9219_CR12","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1023\/A:1019964114625","volume":"15","author":"C Coquand","year":"2002","unstructured":"Coquand, C.: A formalized proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. Higher-Order and Symb. Comp. 15, 57\u201390 (2002)","journal-title":"Higher-Order and Symb. Comp."},{"key":"9219_CR13","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: A formalization of a dependently typed language as an inductive-recursive family. In: Types for Proofs and Programs. Lecture Notes in Computer Science, vol. 4502, pp. 93\u2013109. Springer (2007)","DOI":"10.1007\/978-3-540-74464-1_7"},{"key":"9219_CR14","unstructured":"Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. CUP (1989)"},{"key":"9219_CR15","unstructured":"Goguen, H., McKinna, J.: Candidates for substitution. Tech. Rep. ECS-LFCS-97-358, University of Edinburgh (1997)"},{"issue":"1","key":"9219_CR16","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"9219_CR17","author":"A Hirschowitz","year":"2010","unstructured":"Hirschowitz, A., Maggesi, M.: Nested abstract syntax in Coq. J. Autom. Reason. (2010). doi: 10.1007\/s10817-010-9207-9","journal-title":"J. Autom. Reason."},{"key":"9219_CR18","unstructured":"Hur, C.-K.: Heq: A Coq library for heterogeneous equality. http:\/\/www.mpi-sws.org\/~gil\/Heq\/ (2010). Accessed Feb 2011"},{"key":"9219_CR19","doi-asserted-by":"crossref","unstructured":"Kennedy, A., Russo, C.: Generalized algebraic datatypes and object oriented programming. In: ACM Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA\u201905), pp. 21\u201340. ACM (2005)","DOI":"10.1145\/1103845.1094814"},{"key":"9219_CR20","doi-asserted-by":"crossref","unstructured":"McBride, C.: Elimination with a motive. In: Types for Proofs and Programs. Lecture Notes in Computer Science, vol. 2277, pp. 197\u2013216. Springer (2002)","DOI":"10.1007\/3-540-45842-5_13"},{"key":"9219_CR21","unstructured":"McBride, C.: Type preserving renaming and substitution. http:\/\/strictlypositive.org\/ren-sub.pdf (2005). Accessed Feb 2011"},{"key":"9219_CR22","doi-asserted-by":"crossref","unstructured":"McBride, C.: Outrageous but meaningful coincidences (dependently type-safe syntax and evaluation). In: Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming (WGP\u201910). ACM (2010)","DOI":"10.1145\/1863495.1863497"},{"issue":"1","key":"9219_CR23","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"key":"9219_CR24","doi-asserted-by":"crossref","unstructured":"Sheard, T.: Languages of the future. In: Companion to the 19th ACM Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA\u201904), pp. 116\u2013119. ACM (2004)","DOI":"10.1145\/1028664.1028711"},{"key":"9219_CR25","doi-asserted-by":"crossref","unstructured":"Sozeau, M.: PROGRAM-ing finger trees in COQ. In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP\u201907), pp. 13\u201324. ACM (2007)","DOI":"10.1145\/1291151.1291156"},{"key":"9219_CR26","unstructured":"Sozeau, M.: A dependently-typed formalization of simply-typed lambda-calculus: substitution, denotation, normalization. http:\/\/mattam.org\/research\/publications\/drafts\/lambda-notes.pdf (2007). Accessed Feb 2011"},{"key":"9219_CR27","doi-asserted-by":"crossref","unstructured":"Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201903), pp. 224\u2013235. ACM (2003)","DOI":"10.1145\/604131.604150"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9219-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9219-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9219-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,5]],"date-time":"2023-06-05T12:54:14Z","timestamp":1685969654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9219-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,2]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["9219"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9219-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3,2]]}}}