nits

Manuscript/biblio.bib

@@ -2611,7 +2611,7 @@ @InProceedings{Cockx2020
 }
 
 @Article{Bauer2022,
-  author       = {Andrej Bauer and Anja Petković Komel},
+  author       = {Andrej Bauer and Petković Komel, Anja},
   date         = {2022-01},
   journaltitle = {{Logical Methods in Computer Science}},
   title        = {{An extensible equality checking algorithm for dependent type theories}},
@@ -2621,7 +2621,7 @@ @Article{Bauer2022
   file         = {:Bauer2022 - An Extensible Equality Checking Algorithm for Dependent Type Theories.pdf:PDF},
   groups       = {Conversion, Irrelevance},
   keywords     = {Computer Science - Logic in Computer Science ; Mathematics - Logic ; 03B38 (Primary), 68Q42 (Secondary) ; F.4.1},
-  priority     = {prio1},
+  priority     = {prio2},
 }
 
 @PhdThesis{Dagand2013,
@@ -3797,6 +3797,27 @@ @Eprint{Liesnikov2020
   year      = {2020},
 }
 
+@PhdThesis{PetkovicKomel2021,
+  author      = {Petković Komel, Anja},
+  date        = {2021},
+  institution = {University of Ljubljana},
+  title       = {Meta-analysis of type theories with an application to the design of formal proofs},
+  file        = {:PetkovicKomel2021 - Meta Analysis of Type Theories with an Application to the Design of Formal Proofs.pdf:PDF},
+  priority    = {prio2},
+}
+
+@Thesis{Haselwarter2022,
+  author       = {Haselwarter, Philipp Georg},
+  date         = {2022},
+  institution  = {University of Ljubljana},
+  title        = {Effective metatheory for type theory},
+  type         = {phdthesis},
+  url          = {https://repozitorij.uni-lj.si/IzpisGradiva.php?lang=eng&id=134439},
+  abstractnote = {In this dissertation, I propose finitary type theories as a definition of a wide class of type theories in the style of Martin-Löf, and I design a programming language for deriving judgements in finitary type theories. State of the art computer implementations of type theory rely on a computational interpretation of type theory, either via decidability results or via realisability. Such results are not readily available for all type theories studied in the literature, which renders their implementation challenging. The implementation of a flexible proof assistant supporting user-specified type theories requires a general definition outlining the structure of a type theory. I give a mathematically precise definition of a class of finitary type theories, that covers familiar examples, including Extensional Type Theory, the Calculus of Constructions, and Homotopy Type Theory. I first focus on the mathematical development of finitary type theories, before turning to their implementation in proof assistants. The definition proceeds in stages, starting with raw syntax, raw rules, and raw type theories, then delineating finitary rules and type theories, and finally specifying standard type theories. Once these definitions are accomplished, general meta-theoretic results in the form of a uniqueness of typing theorem and a cut elimination theorem are proved. I reformulate finitary type theories with a suitable treatment of free variables as context-free type theories, paving the way to an implementation in a proof assistant. The definition of context-free type theories again proceeds in stages of refinement, and I prove metatheorems for each successive stage. Translation theorems between context-free and finitary type theories relate the two formalisms. I introduce the Andromeda metalanguage (AML), an effectful programming language that allows convenient manipulation of judgement and rules of user-definable context-free type theories, and supports common proof development techniques. AML leverages algebraic effects and runners to extend proof assistant algorithms with local hypothesis in a modular way. The operational semantics of AML is inspired by bidirectional typing and helps the user harness contextual information, exhibiting a virtuous interaction with effect operations. AML has been implemented in the Andromeda prover, and I describe first experiments in the computer-assisted development of context-free type theories in AML.},
+  file         = {:Haselwarter2022 - Effective Metatheory for Type Theory.pdf:PDF},
+  priority     = {prio2},
+}
+
 @Comment{jabref-meta: databaseType:biblatex;}
 
 @Comment{jabref-meta: grouping:

Manuscript/styles/layout.sty

@@ -44,50 +44,6 @@
 % \addtokomafont{subsection}{\color{LightGreen}}
 % \addtokomafont{subsubsection}{\color{LightGreen}}
 
+% Misc
 
-%% Tables
-
-% \RequirePackage{diagbox} %For diagonal slash in a table
-
-%% Paragraphs
-
-%\RequirePackage{indentfirst} %To indent the first paragraph of a new section
-% \usepackage{ragged2e} %For better ragged/centered environments
-
-%% Changing the style of floats
-
-% \RequirePackage{float}
-% \floatstyle{boxed}
-% \restylefloat{figure}
-
-%% Titles (taken from M2 internship)
-
-% \usepackage{titlesec}
-
-% \titleformat{\section}
-% 	{\Large \bfseries}
-% 	{\hspace{1em}\thetitle.}
-% 	{1ex}
-% 	{}
-% [\titlerule]
-% \titlespacing*{\section}{0em}{2em}{2em}
-
-% \titleformat{\subsection}
-% {\Large \bfseries}
-% {\thetitle.}
-% {1ex}
-% {}
-% \titlespacing*{\subsection}{0em}{1em}{1em}
-
-% \titleformat{\paragraph}[runin]{\scshape}{}{0pt}{}
-% \titlespacing{\paragraph}{0pt}{*2}{2\wordsep}
-
-%% Theorems, already present in kao but may need modifications
-
-% \RequirePackage[thmmarks, framed]{ntheorem}
-% \RequirePackage[ntheorem=true]{mdframed}
-
-%% Bibliography
-
-% \RequirePackage[backend=biber,style=alphabetic,citestyle=alphabetic]{biblatex}
-% \ExecuteBibliographyOptions{giveninits=true}
+\usepackage{comment}