{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T00:38:29Z","timestamp":1760575109547,"version":"build-2065373602"},"reference-count":22,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.431.6","type":"journal-article","created":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T09:32:32Z","timestamp":1760347952000},"page":"82-98","source":"Crossref","is-referenced-by-count":0,"title":["Dependently Sorted Nominal Signatures"],"prefix":"10.4204","volume":"431","author":[{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"first","affiliation":[{"name":"King s College London, UK"}]},{"given":"Miguel","family":"Pagano","sequence":"additional","affiliation":[{"name":"FAMAF - Universidad Nacional de C\u00f3rdoba, Argentina"}]},{"given":"Nora","family":"Szasz","sequence":"additional","affiliation":[{"name":"Universidad ORT Uruguay"}]},{"given":"\u00c1lvaro","family":"Tasistro","sequence":"additional","affiliation":[{"name":"Universidad ORT Uruguay"}]}],"member":"2720","published-online":{"date-parts":[[2025,10,14]]},"reference":[{"key":"AdamsR:lamfree","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.0804.1879","article-title":"Lambda-Free Logical Frameworks","volume":"abs\/0804.1879","author":"Adams","year":"2008","journal-title":"CoRR"},{"key":"BarendregtH:lamcss","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: its Syntax and Semantics (revised ed.)","volume":"103","author":"Barendregt","year":"1984"},{"key":"Beluga","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-03545-1_16","article-title":"Programming Type-Safe Transformations Using Higher-Order Abstract Syntax","volume-title":"Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings","volume":"8307","author":"B\u00e9langer","year":"2013"},{"issue":"2","key":"DBLP:journals\/em\/BordgPL22","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1080\/10586458.2022.2062073","article-title":"Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types","volume":"31","author":"Bordg","year":"2022","journal-title":"Exp. Math."},{"key":"Cartmell86","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","article-title":"Generalised algebraic theories and contextual categories","volume":"32","author":"Cartmell","year":"1986","journal-title":"Ann. Pure Appl. Log."},{"key":"CheneyJ:sntt","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/J.ENTCS.2008.12.115","article-title":"A Simple Nominal Type Theory","volume":"228","author":"Cheney","year":"2009","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"CheneyJ:depntt","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:8)2012","article-title":"A dependent nominal type theory","volume":"8","author":"Cheney","year":"2012","journal-title":"Logical Methods in Computer Science"},{"issue":"5","key":"CheneyJ:alpp","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675","article-title":"Nominal logic programming","volume":"30","author":"Cheney","year":"2008","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"FairweatherE:deptnt","series-title":"LIPIcs","doi-asserted-by":"publisher","first-page":"180","DOI":"10.4230\/LIPICS.TLCA.2015.180","article-title":"Dependent Types for Nominal Terms with Atom Substitutions","volume-title":"13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland","volume":"38","author":"Fairweather","year":"2015"},{"key":"Fiore08","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/LICS.2008.38","article-title":"Second-Order and Dependently-Sorted Abstract Syntax","volume-title":"Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA","author":"Fiore","year":"2008"},{"key":"gabbay:nomtnl","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-94-007-6600-6_2","article-title":"Nominal terms and nominal logics: from foundations to meta-mathematics","volume-title":"Handbook of Philosphical Logic","volume":"17","author":"Gabbay","year":"2011"},{"key":"gabbay:capasn-jv","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/11921240_14","article-title":"Capture-Avoiding Substitution as a Nominal Algebra","volume":"20","author":"Gabbay","year":"2008","journal-title":"Formal Aspects of Computing"},{"issue":"4","key":"gabbay:oneaah-jv","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1093\/logcom\/exm064","article-title":"One-and-a-halfth-order Logic","volume":"18","author":"Gabbay","year":"2008","journal-title":"Journal of Logic and Computation"},{"key":"gabbay:curhid","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-540-69937-8_16","article-title":"One-and-a-halfth Order Terms: Curry-Howard for Incomplete Derivations","volume-title":"Proceedings of 15th Workshop on Logic, Language and Information in Computation (WoLLIC 2008)","volume":"5110","author":"Gabbay","year":"2008"},{"key":"harper:fradl","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1145\/138027.138060","article-title":"A Framework for Defining Logics","volume-title":"Proceedings of the 2nd IEEE Symposium on Logic in Computer Science (LICS 1987)","author":"Harper","year":"1987"},{"key":"KaposiX24","series-title":"LIPIcs","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2024.10","article-title":"Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics","volume-title":"9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia","volume":"299","author":"Kaposi","year":"2024"},{"issue":"2","key":"pitts:nomlfo-jv","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","article-title":"Nominal Logic, A First Order Theory of Names and Binding","volume":"186","author":"Pitts","year":"2003","journal-title":"Information and Computation"},{"issue":"3","key":"pitts:alpsri","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/1147954.1147961","article-title":"Alpha-structural recursion and induction","volume":"53","author":"Pitts","year":"2006","journal-title":"Journal of the ACM"},{"key":"PittsA:deptta","series-title":"Electronic Notes in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/J.ENTCS.2015.04.003","article-title":"A Dependent Type Theory with Abstractable Names","volume-title":"Ninth Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2014, Bras\u00edlia, Brazil, September 8-9, 2014","volume":"312","author":"Pitts","year":"2014"},{"key":"SterlingJ:algttu","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1902.08848","article-title":"Algebraic Type Theory and Universe Hierarchies","volume":"abs\/1902.08848","author":"Sterling","year":"2019","journal-title":"CoRR"},{"volume-title":"Abstract and concrete type theories","year":"2021","author":"Uemura","key":"UemuraPhD"},{"key":"UrbanC:nomu-jv","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","article-title":"Nominal Unification","volume":"323","author":"Urban","year":"2004","journal-title":"Theoretical Computer Science"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T11:11:23Z","timestamp":1760526683000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2510.12305v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,14]]},"references-count":22,"URL":"https:\/\/doi.org\/10.4204\/eptcs.431.6","relation":{},"ISSN":["2075-2180"],"issn-type":[{"type":"electronic","value":"2075-2180"}],"subject":[],"published":{"date-parts":[[2025,10,14]]}}}