{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T17:27:48Z","timestamp":1760549268141,"version":"3.41.2"},"reference-count":41,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,2,20]],"date-time":"2012-02-20T00:00:00Z","timestamp":1329696000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Nominal abstract syntax is an approach to representing names and binding pioneered by Gabbay and Pitts. So far nominal techniques have mostly been studied using classical logic or model theory, not type theory. Nominal extensions to simple, dependent and ML-like polymorphic languages have been studied, but decidability and normalization results have only been established for simple nominal type theories. We present a LF-style dependent type theory extended with name-abstraction types, prove soundness and decidability of beta-eta-equivalence checking, discuss adequacy and canonical forms via an example, and discuss extensions such as dependently-typed recursion and induction principles.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:8)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":10,"title":["A dependent nominal type theory"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1307-9286","authenticated-orcid":false,"given":"James","family":"Cheney","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,2,20]]},"reference":[{"key":"10.2168\/LMCS-8(1:8)2012_appel92compiling","doi-asserted-by":"crossref","unstructured":"A. Appel.Compiling with Continuations. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511609619"},{"key":"10.2168\/LMCS-8(1:8)2012_avron92jar","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron, F. Honsell, I. A. Mason, and R","year":"1992","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"10.2168\/LMCS-8(1:8)2012_DBLP:journals\/jfp\/BucaloHMSH06","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1017\/S0956796806005892","volume":"16","author":"A. Bucalo, F. Honsell, M. Miculan, I. Sc","year":"2006","journal-title":"J. Funct. Program."},{"key":"10.2168\/LMCS-8(1:8)2012_cheney05icfp","doi-asserted-by":"crossref","unstructured":"J. Cheney. Scrap your nameplate (functional pearl). In B. Pierce, editor,Proceedings of the 10th International Conference on Functional Programming (ICFP 2005), pages 180-191, Tallinn, Estonia, 2005. ACM.","DOI":"10.1145\/1090189.1086389"},{"key":"10.2168\/LMCS-8(1:8)2012_cheney08lfmtp","first-page":"37","volume":"228","author":"J. Cheney","year":"2009","journal-title":"ENTCS Proceedings of LFMTP 2008"},{"key":"10.2168\/LMCS-8(1:8)2012_cheney11jar","doi-asserted-by":"crossref","unstructured":"J. Cheney, R. Vestergaard, and M. Norrish. Formalizing adequacy: a case study for higher-order abstract syntax.Journal of Automated Reasoning, 2011. To appear. Published online March 2011.","DOI":"10.1007\/s10817-011-9221-6"},{"key":"10.2168\/LMCS-8(1:8)2012_crary08lfmtp","first-page":"53","volume":"228","author":"K. Crary","year":"2009","journal-title":"ENTCS Proceedings of LFMTP 2008"},{"key":"10.2168\/LMCS-8(1:8)2012_despeyroux95tlca","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014049"},{"key":"10.2168\/LMCS-8(1:8)2012_despeyroux94lpar","doi-asserted-by":"crossref","unstructured":"J. Despeyroux and A. Hirschowitz. Higher-order abstract syntax with induction in Coq. InLPAR, pages 159-173, 1994.","DOI":"10.1007\/3-540-58216-9_36"},{"key":"10.2168\/LMCS-8(1:8)2012_gabbay02fac","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M. J. Gabbay and A. M. Pitts","year":"2002","journal-title":"Formal Aspects of Computing"},{"issue":"4","key":"10.2168\/LMCS-8(1:8)2012_geuvers99mscs","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1017\/S0960129599002856","volume":"9","author":"H. Geuvers and E. Barendsen","year":"1999","journal-title":"Mathematical structures in computer science 1999"},{"key":"10.2168\/LMCS-8(1:8)2012_hannan95tpa","unstructured":"J. Hannan. Type systems for closure conversions. In H. R. Nielson and K. L. Solberg, editors,Participants' Proceedings of the Workshop on Types for Program Analysis, pages 48-62, 1995. Technical Report DAIMI PB-493, Aarhus University."},{"key":"10.2168\/LMCS-8(1:8)2012_harel00","doi-asserted-by":"crossref","unstructured":"D. Harel, D. Kozen, and J. Tiuryn.Dynamic Logic. MIT Press, 2000.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"issue":"1","key":"10.2168\/LMCS-8(1:8)2012_harper93jacm","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper, F. Honsell, and G. Plotkin","year":"1993","journal-title":"Journal of the Association for Computing Machinery 40(1):143-184, January 1993"},{"issue":"1","key":"10.2168\/LMCS-8(1:8)2012_harper05tocl","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1145\/1042038.1042041","volume":"6","author":"R. Harper and F. Pfenning","year":"2005","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.2168\/LMCS-8(1:8)2012_honsell96types","doi-asserted-by":"crossref","unstructured":"F. Honsell and M. Miculan. A natural deduction approach to dynamic logic. InTYPES, volume 1158 ofLecture Notes in Computer Science, pages 165-182, 1996.","DOI":"10.1007\/3-540-61780-9_69"},{"issue":"2","key":"10.2168\/LMCS-8(1:8)2012_honsell01tcs","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell, M. Miculan, and I. Scagnetto","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(1:8)2012_maclane92sheaves","unstructured":"S. M. Lane and I. Moerdijk.Sheaves in geometry and logic: a first introduction to topos theory. Springer-Verlag, 1992."},{"key":"10.2168\/LMCS-8(1:8)2012_licata08lics","doi-asserted-by":"crossref","unstructured":"D. R. Licata, N. Zeilberger, and R. Harper. Focusing on binding and computation. InLICS, pages 241-252. IEEE Computer Society, 2008.","DOI":"10.1109\/LICS.2008.48"},{"key":"10.2168\/LMCS-8(1:8)2012_mason87lfcs","unstructured":"I. A. Mason. Hoare's logic in the LF. Technical Report ECS-LFCS-87-32, University of Edinburgh, 1987."},{"key":"10.2168\/LMCS-8(1:8)2012_miculan05merlin","doi-asserted-by":"crossref","unstructured":"M. Miculan, I. Scagnetto, and F. Honsell. Translating specifications from nominal logic to CIC with the theory of contexts. In R. Pollack, editor,Proceedings of the 3rd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2005), pages 41-49, Tallinn, Estonia, September 2005. ACM Press.","DOI":"10.1145\/1088454.1088460"},{"issue":"4","key":"10.2168\/LMCS-8(1:8)2012_miller05tocl","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D. Miller and A. Tiu","year":"2005","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.2168\/LMCS-8(1:8)2012_nadathur98higher","doi-asserted-by":"crossref","unstructured":"G. Nadathur and D. Miller. Higher-order logic programming. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors,Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, chapter 8, pages 499-590. Oxford University Press, 1998.","DOI":"10.1093\/oso\/9780198537922.003.0011"},{"key":"10.2168\/LMCS-8(1:8)2012_odersky94popl","doi-asserted-by":"crossref","unstructured":"M. Odersky. A functional theory of local names. InProc. 21st ACM Symposium on Principles of Programming Languages, pages 48-59, January 1994.","DOI":"10.1145\/174675.175187"},{"issue":"2","key":"10.2168\/LMCS-8(1:8)2012_ohearn99bsl","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P. O'Hearn and D. J. Pym","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.2168\/LMCS-8(1:8)2012_pfenning89pldi","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Elliott. Higher-order abstract syntax. InProceedings of the 1989 ACM SIGPLANConf. on {Programming Language Design and Implementation (PLDI '89)}, pages 199-208. ACM Press, 1989.","DOI":"10.1145\/960116.54010"},{"key":"10.2168\/LMCS-8(1:8)2012_pientka08popl","doi-asserted-by":"crossref","unstructured":"B. Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. InPOPL, pages 371-382, 2008.","DOI":"10.1145\/1328897.1328483"},{"issue":"3","key":"10.2168\/LMCS-8(1:8)2012_pitts06jacm","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1145\/1147954.1147961","volume":"53","author":"A. M. Pitts","year":"2006","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-8(1:8)2012_pitts10popl","doi-asserted-by":"crossref","unstructured":"A. M. Pitts. Nominal system T. InPOPL, pages 159-170, 2010.","DOI":"10.1145\/1707801.1706321"},{"issue":"3","key":"10.2168\/LMCS-8(1:8)2012_pitts11jfp","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1017\/S0956796811000116","volume":"21","author":"A. M. Pitts","year":"2011","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-8(1:8)2012_poswolsky08esop","doi-asserted-by":"crossref","unstructured":"A. Poswolsky and C. Sch\u00fcrmann. Practical programming with higher-order encodings and dependent types. InESOP, number 4960 in LNCS, pages 93-107, 2008.","DOI":"10.1007\/978-3-540-78739-6_7"},{"key":"10.2168\/LMCS-8(1:8)2012_pottier07lics","doi-asserted-by":"crossref","unstructured":"F. Pottier. Static name control for FreshML. InLICS 2007, pages 356-365, Wroclaw, Poland, July 2007.","DOI":"10.1109\/LICS.2007.44"},{"key":"10.2168\/LMCS-8(1:8)2012_poulliard10icfp","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863575"},{"key":"10.2168\/LMCS-8(1:8)2012_schoepp06phd","unstructured":"U. Sch\u00f6pp.Names and Binding in Type Theory. PhD thesis, University of Edinburgh, 2006."},{"issue":"5","key":"10.2168\/LMCS-8(1:8)2012_schoepp06lfmtp","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.entcs.2007.01.027","volume":"174","author":"U. Sch\u00f6pp","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science 174(5):19-35, 2007"},{"key":"10.2168\/LMCS-8(1:8)2012_schoepp04csl","doi-asserted-by":"crossref","unstructured":"U. Sch\u00f6pp and I. Stark. A dependent type theory with names and binding. InCSL 2004, number 3210 in LNCS, pages 235-249, Karpacz, Poland, 2004.","DOI":"10.1007\/978-3-540-30124-0_20"},{"issue":"1-2","key":"10.2168\/LMCS-8(1:8)2012_schuermann01tcs","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(00)00418-7","volume":"266","author":"C. Sch\u00fcrmann, J. Despeyroux, and F. Pfen","year":"2001","journal-title":"Theor. Comput. Sci."},{"key":"10.2168\/LMCS-8(1:8)2012_shinwell03icfp-short","doi-asserted-by":"crossref","unstructured":"M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. FreshML: Programmming with binders made simple. InICFP, pages 263-274. ACM Press, 2003.","DOI":"10.1145\/944746.944729"},{"key":"10.2168\/LMCS-8(1:8)2012_urban11tocl","first-page":"15","volume":"12","author":"C. Urban, J. Cheney, and S. Berghofer","year":"2011","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.2168\/LMCS-8(1:8)2012_westbrook08phd","unstructured":"E. Westbrook.Higher-order encodings with constructors. PhD thesis, Washington University in St. Louis, 2008."},{"key":"10.2168\/LMCS-8(1:8)2012_westbrook09lfmtp","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577836"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1042\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1042\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,25]],"date-time":"2023-06-25T15:58:42Z","timestamp":1687708722000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1042"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,20]]},"references-count":41,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:8)2012","relation":{"references":[{"id-type":"doi","id":"10.1145\/1577824.1577836","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1201.5240","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1201.5240","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,2,20]]},"article-number":"1042"}}