Much of the work presented in these notes are based on existing work,

Intrinsically-typed terms is based on:

Guillaume Allais, James Chapman, Conor McBride, and James McKinna. 2017. Type-and-scope safe programs and their proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). Association for Computing Machinery, New York, NY, USA, 195–207. https://doi.org/10.1145/3018610.3018613

Evaluation through definitional interpretation based on:

Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2017. Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang. 2, POPL, Article 16 (January 2018), 34 pages. https://doi.org/10.1145/3158104

Elaboration is based on Chapters Lambda and Inference from

Wadler, Philip, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Available at https://plfa.inf.ed.ac.uk/22.08/. 2022.

Additionally other material on intrinsically-typed terms is from the same material. Specifically the chapters named De Bruijn and More (De Bruijn).