20.500.12556/RUL-152580 Finitary type theories with and without contexts We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin–Löf 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. dependent type theory context-free type theory formal meta-theory proof assistants true false true Angleški jezik Ni določen Članek v reviji 2023-11-29 12:30:19 2023-11-29 12:30:23 2023-11-30 03:42:11 0000-00-00 00:00:00 2023 0 0 87 str. iss. 4, art. 36 Vol. 67 Dec. 2023 0000-00-00 Zaloznikova Objavljeno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 0168-7433 10.1007/s10817-023-09678-y 168229379 s10817-023-09678-y.pdf s10817-023-09678-y.pdf 1 DF23C58AFCB26D04757B2CB6AA923527 4b7e12f0dfcb3ed9bb7984612ea2625f02ec617990c042122b8f41f59f3156f9 edddd1ca-8eaa-11ee-9c6c-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=178130 https://link.springer.com/article/10.1007/s10817-023-09678-y 1 b0fd83d0-8eaa-11ee-9c6c-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=178129 Fakulteta za matematiko in fiziko 0 0 0