@article{NBE2016,
	title={Normalisation by Evaluation for Dependent Types},
	author={Thorsten Altenkirch and Ambrus Kaposi},
	booktitle={International Conference on Formal Structures for Computation and Deduction},
	year={2016}
}
@phdthesis{AltenkirschThesis1993,
	title={Constructions, inductive types and strong normalization},
	author={Thorsten Altenkirch},
	booktitle={CST},
	year={1993}
}
@unpublished{TaoOfTypes,
	title={The Tao of Types},
	author={Thorsten Altenkirsch}
}
@inproceedings{folSogatKaposi2023,
	title={Why is equality interesting?},
	author={Ambrus Kaposi},
	url={https://akaposi.github.io/pres_wld.pdf}}

@phdthesis{UemuraThesis2021,
	title = {Abstract and concrete type theories},
	isbn = {9789464213768},
	url = {https://dare.uva.nl/search?identifier=41ff0b60-64d4-4003-8182-c244a9afab3b},
	language = {en},
	urldate = {2023-08-04},
	publisher = {AmsterdamInstitute for Logic, Language and Computation},
	author = {Uemura, T.},
	year = {2021},
}

@article{logicalFramework1993,
	author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon},
	title = {A Framework for Defining Logics},
	year = {1993},
	issue_date = {Jan. 1993},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {40},
	number = {1},
	issn = {0004-5411},
	url = {https://doi.org/10.1145/138027.138060},
	doi = {10.1145/138027.138060},
	abstract = {The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-Lo¨f's system of arities. The treatment of rules and proofs focuses on his notion of a judgment. Logics are represented in LF via a new principle, the judgments as types principle, whereby each judgment is identified with the type of its proofs. This allows for a smooth treatment of discharge and variable occurence conditions and leads to a uniform treatment of rules and proofs whereby rules are viewed as proofs of higher-order judgments and proof checking is reduced to type checking. The practical benefit of our treatment of formal systems is that logic-independent tools, such as proof editors and proof checkers, can be constructed.},
	journal = {J. ACM},
	month = {jan},
	pages = {143–184},
	numpages = {42},
	keywords = {formal systems, interactive theorem proving, proof checking, typed lambda calculus}
}

@article{hoffmann1999,
	author = {Hofmann, Martin},
	title = {Semantical Analysis of Higher-Order Abstract Syntax},
	year = {1999},
	isbn = {0769501583},
	publisher = {IEEE Computer Society},
	address = {USA},
	abstract = {A functor category semantics for higher-order abstract syntax is proposed with the following aims: relating higher-order and first order syntax, justifying induction principles, suggesting new logical principles to reason about higher-order syntax},
	booktitle = {Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science},
	pages = {204},
	series = {LICS '99}
}

@article{fioreMahmoud2013secondorder,
	title={Second-Order Algebraic Theories}, 
	author={Marcelo Fiore and Ola Mahmoud},
	year={2013},
	eprint={1308.5409},
	archivePrefix={arXiv},
	primaryClass={cs.LO}
}
@article{RedFreeNorm1995,
	doi = {10.1007/3-540-60164-3_27},
	url = {https://doi.org/10.1007\3-540-60164-3_27},
	year = 1995,
	publisher = {Springer Berlin Heidelberg},
	pages = {182--199},
	author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
	title = {Categorical reconstruction of a reduction free normalization proof},
	booktitle = {Category Theory and Computer Science}
}