This started as a Twiter reply to @slimjimmy_dev asking for some resources to help understand my Lean formalization of the untyped lambda calculusNow that the groundwork is laid I should be able tackle the categorical semantics of the untyped lambda calculus in Lean next! I claim no originality for the confluence/progress pieces, they are an amalgamation of the resources listed in this article., but quickly grew long enough that I decided to make it into a post. Formalizing metatheory is a topic that is interesting to beginner and experienced proof assistant users alike, but rife with tricky technical issues that can dissuade one from making much progress. I hope by collecting some resources here that I can provide a bit of help to those looking for where to get started. The first tip that I would give is that it is very useful to be “multilingual” with respect to proof assistants. Lean and Rocq are close enough that you can reasonably transfer knowledge between the two, but it is immensely helpful to also have enough working knowledge of Agda to be able to at least read along and translate other formalizations into your proof assistant of choice. The first resource I’ll mention is Software Foundations, Volume 2: Programming Language Foundations. As with the entirety of the series, it is carefully structured and accompanied with well-written explanations that make it a good starting point. It walks through a formalization of the simply typed lambda calculus (STLC), as well as a few extensions. One of the reasons that this is a useful and interesting resource from the pedagogy perspective is its treatment of variable binding and substitution. It takes the approach of treating bindings as strings, but combines this with some simplifying assumptions that make substitution not as difficult to work with. It also has the benefit of explicitly referring to chapters of Types and Programming Languages, which can be helpful for learning to connect informal and formal definitions. In general, this is not the approach that formalizations take. To understand why, consider the terms ((\lambda x , . , x)) and ((\lambda y , . , y)). These are (\alpha)-equivalent, meaning they are the same up to a consistent replacement of variable names. However, from the perspective of a formalization that treats variable bindings as strings, they are not definitionally equal terms from the perspective of the proof assistant. The usual approach here is to use de Bruijn indices, where a variable is instead represented by a natural number that indicates how far away its binding is. Now, the two terms above both become represented by ((\lambda , . , 0)), and we can use the proof assistant’s notion of equality. Another issue (in typed systems) is the idea of typing being extrinsic or intrinsic. In Software Foundations types and terms are defined separately (extrinsic), while another approach would be to find a way to define a single inductive type that only permits well-typed terms (intrinsic). A resource that addresses these two ideas is Part 2 of Programming Language Foundations in Agda. It covers some of the same ground as Software Foundations, but takes the approach of formalizing STLC using both de Bruijn indices and intrinsic typing. Another valuable contribution of PLFA is that it also formalizes the untyped lambda calculus and its property of confluence, the idea that we can pick any order of reductions and eventually converge back to the same term. In practice however, it can be very painful to work with de Bruijn indices. When we construct terms and perform substitutions, we are required to “shift” these indices, and lemmas related to the behavior of this shifting can be quite cumbersome. An alternative approach is to define the syntax of our lambda calculus terms to differentiate between bound and free variables. We still must prove some lemmas regarding how different operations on free and bound variables interact, but this is much less arduous. This Rocq tutorial from the Penn PL Club serves as a great introduction to this approach, including both simple types and System F(_{<:}). Another tip is to scour GitHub for as many examples of formalizations as possible, as it is helpful to see the slight variations in formalization and proof structure. Eventually, as you grow more comfortable, you will be able to mix and match according to your needs and preferences. Here are additional repos and resources that I have found helpful: