12. Acknowledgements

Many people have made helpful suggestions about this material, or have helped us in other ways. Tom Ball and Leo DeMoura encoured me to pursue this line of work, for which I thank them. They along with Jeremy Avigad answered many questions I had about Lean in the early days of this work. Jeremy Avigad and his colleagues graciously allowed me to use the Sphinx infrastructure they built to format this material. Corrections and other very helpful feedbak have been given by many people: Jim Cohoon, Nathan Brunelle, Patrick Massot, Moses Schönfinkel, Scott Morrison, …, and my wonderful students, both undergraduate and graduate, here at UVa.