{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:24Z","timestamp":1740123324695,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T00:00:00Z","timestamp":1696636800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T00:00:00Z","timestamp":1696636800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-14-1-0096","FA9550-21-1-0024"],"award-info":[{"award-number":["FA9550-14-1-0096","FA9550-21-1-0024"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin\u2013L\u00f6f type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly annotated with their types. We provide translations between finitary type theories with and without contexts, thereby showing that they have the same expressive power. The context-free type theory is implemented in the nucleus of the Andromeda 2 proof assistant.<\/jats:p>","DOI":"10.1007\/s10817-023-09678-y","type":"journal-article","created":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T08:02:36Z","timestamp":1696665756000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Finitary Type Theories With and Without Contexts"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0198-7751","authenticated-orcid":false,"given":"Philipp G.","family":"Haselwarter","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5378-0547","authenticated-orcid":false,"given":"Andrej","family":"Bauer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,10,7]]},"reference":[{"key":"9678_CR1","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume":"90","author":"P Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definitions. Stud. Logic Found. Math. 90, 739\u2013782 (1977)","journal-title":"Stud. Logic Found. Math."},{"issue":"1","key":"9678_CR2","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/2914770.2837638","volume":"51","author":"T Altenkirch","year":"2016","unstructured":"Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. ACM SIGPLAN Notices 51(1), 18\u201329 (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"9678_CR3","doi-asserted-by":"publisher","unstructured":"Angiuli, C., Hou\u00a0(Favonia), K.-B., Harper, R.: Cartesian cubical computational type theory: constructive reasoning with paths and equalities. In: Ghica, D., Jung, A. (eds.) CSL 2018 (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.6","DOI":"10.4230\/LIPIcs.CSL.2018.6"},{"key":"9678_CR4","unstructured":"Annenkov, D., Capriotti, P., Kraus, N., Sattler, C.: Two-level type theory and applications. arXiv:1705.03307 (2019)"},{"key":"9678_CR5","doi-asserted-by":"publisher","unstructured":"Bauer, A., Gilbert, G., Haselwarter, P.G., Pretnar, M., Stone, C.A.: Design and implementation of the andromeda proof assistant. In: TYPES\u201916 (2018). https:\/\/doi.org\/10.4230\/lipics.types.2016.5","DOI":"10.4230\/lipics.types.2016.5"},{"key":"9678_CR6","unstructured":"Bauer, A., Haselwarter, P.G., Lumsdaine, P.L.: A general definition of dependent type theories. arXiv:2009.05539 (2020)"},{"key":"9678_CR7","doi-asserted-by":"crossref","unstructured":"Bauer, A., Petkovi\u0107 Komel, A.: An extensible equality checking algorithm for dependent type theories. arXiv:2103.07397 (2021)","DOI":"10.46298\/lmcs-18(1:17)2022"},{"key":"9678_CR8","doi-asserted-by":"publisher","unstructured":"Birkedal, L., Nuyts, A., Kavvos, G.A., Gratzer, D.: Multimodal dependent type theory. In: Logical Methods in Computer Science (2021). https:\/\/doi.org\/10.46298\/lmcs-17(3:11)2021","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"9678_CR9","unstructured":"Bocquet, R., Kaposi, A., Sattler, C.: Relative induction principles for type theories. arxiv:2102.11649 (2021)"},{"key":"9678_CR10","unstructured":"Capriotti, P.: Models of type theory with strict equality. PhD thesis, University of Nottingham (2016). arxiv:1702.04912"},{"key":"9678_CR11","unstructured":"Cartmell, J.W.: Generalised algebraic theories and contextual categories. PhD thesis, University of Oxford (1978)"},{"key":"9678_CR12","doi-asserted-by":"publisher","unstructured":"Cavallo, E., M\u00f6rtberg, A., Swan, A.W.: Unifying cubical models of univalent type theory. In: CSL 2020 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.14","DOI":"10.4230\/LIPIcs.CSL.2020.14"},{"issue":"1","key":"9678_CR13","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1006\/inco.2001.2951","volume":"179","author":"I Cervesato","year":"2002","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19\u201375 (2002). https:\/\/doi.org\/10.1006\/inco.2001.2951","journal-title":"Inf. Comput."},{"key":"9678_CR14","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 49, 363\u2013408 (2012)","journal-title":"J. Autom. Reason."},{"key":"9678_CR15","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. arXiv:1611.02108 (2016)"},{"key":"9678_CR16","doi-asserted-by":"publisher","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the Lambda-Pi-calculus modulo. In: Della\u00a0Rocca, S.R. (ed.) Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, pp. 102\u2013117 (2007). https:\/\/doi.org\/10.1007\/978-3-540-73228-0_9","DOI":"10.1007\/978-3-540-73228-0_9"},{"issue":"5","key":"9678_CR17","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG de Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math. 75(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"9678_CR18","unstructured":"Fiore, M., Mahmoud, O.: Functorial semantics of second-order algebraic theories. arxiv:1401.4697 (2014)"},{"key":"9678_CR19","doi-asserted-by":"publisher","first-page":"53","DOI":"10.4204\/EPTCS.34.6","volume":"34","author":"H Geuvers","year":"2010","unstructured":"Geuvers, H., Krebbers, R., McKinna, J., Wiedijk, F.: Pure type systems without explicit contexts. Electron. Proc. Theoret. Comput. Sci. 34, 53\u201367 (2010). https:\/\/doi.org\/10.4204\/EPTCS.34.6","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"key":"9678_CR20","doi-asserted-by":"crossref","unstructured":"Gratzer, D.: Normalization for multimodal type theory. arXiv:2106.01414 (2021)","DOI":"10.1145\/3531130.3532398"},{"key":"9678_CR21","unstructured":"Harper, R.: An equational logical framework for type theories. arXiv:2106.01484 (2021)"},{"issue":"1","key":"9678_CR22","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0304-3975(90)90108-T","volume":"89","author":"R Harper","year":"1991","unstructured":"Harper, R., Pollack, R.: Type checking with universes. Theoret. Comput. Sci. 89(1), 107\u2013136 (1991)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"9678_CR23","doi-asserted-by":"publisher","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":"9678_CR24","unstructured":"Haselwarter, P.G.: Effective metatheory of type theory. PhD thesis, University of Ljubljana. https:\/\/repozitorij.uni-lj.si\/IzpisGradiva.php?id=134439 &lang=eng (2021)"},{"key":"9678_CR25","unstructured":"Isaev, V.: Algebraic presentations of dependent type theories. arxiv:1602.08504 (2016)"},{"key":"9678_CR26","unstructured":"Luo, Z.: An extended calculus of constructions. PhD thesis, University of Edinburgh (1990)"},{"key":"9678_CR27","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Studies in Logic and the Foundations of Mathematics, vol. 104, pp. 153\u2013175 (1982)","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"9678_CR28","unstructured":"McKinna, J., Pollack, R.: Pure type systems formalized. In: TLCA, vol. 664 (1993)"},{"key":"9678_CR29","unstructured":"Petkovi\u0107 Komel, A.: Towards an Elaboration Theorem. HoTT\/UF, Invited Talk (2021)"},{"key":"9678_CR30","unstructured":"Petkovi\u0107\u00a0Komel, A.: Meta-analysis of type theories with an application to the design of formal proofs. PhD thesis, University of Ljubljana. https:\/\/repozitorij.uni-lj.si\/IzpisGradiva.php?id=134058 &lang=eng (2021)"},{"key":"9678_CR31","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2014a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Automated Deduction\u2014CADE-16. Lecture Notes in Computer Science, pp. 202\u2013206 (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14","DOI":"10.1007\/3-540-48660-7_14"},{"key":"9678_CR32","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1063\u20131147 (2001)","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"9678_CR33","doi-asserted-by":"crossref","unstructured":"Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: International Joint Conference on Automated Reasoning, pp. 15\u201321 (2010)","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"9678_CR34","doi-asserted-by":"publisher","first-page":"109","DOI":"10.4204\/EPTCS.158.8","volume":"158","author":"U Schreiber","year":"2014","unstructured":"Schreiber, U., Shulman, M.: Quantum gauge field theory in cohesive Homotopy type theory. Electron. Proc. Theoret. Comput. Sci. 158, 109\u2013126 (2014). https:\/\/doi.org\/10.4204\/EPTCS.158.8","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"key":"9678_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6","volume-title":"Semantics of Type Theory. Progress in Theoretical Computer Science","author":"T Streicher","year":"1991","unstructured":"Streicher, T.: Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhaauser, Basel (1991)"},{"issue":"2","key":"9678_CR36","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"key":"9678_CR37","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, vol. 43, 2nd edn. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (2000)","edition":"2"},{"key":"9678_CR38","unstructured":"Uemura, T.: A general framework for the semantics of type theory. arXiv:1904.04097 (2019)"},{"key":"9678_CR39","unstructured":"Voevodsky, V.: HTS\u2014a simple type system with two identity types (2013)"},{"key":"9678_CR40","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A Concurrent Logical Framework I: Judgments and Properties. Technical report, Carnegie Mellon University (2003)","DOI":"10.21236\/ADA418517"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09678-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09678-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09678-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,9]],"date-time":"2023-12-09T09:05:27Z","timestamp":1702112727000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09678-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,7]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["9678"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09678-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,10,7]]},"assertion":[{"value":"1 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 October 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"36"}}