Referencias

Subconjunto de la bibliografía de la tesis: las obras citadas en las páginas publicadas de esta guía. Para la lista completa, véase el documento original.

• Avigad, J., de Moura, L. y Kong, S. (2015). Theorem Proving in Lean. Carnegie Mellon University. https://leanprover.github.io/theorem_proving_in_lean4/
• Barendregt, H. (1991). Introduction to generalized type systems. Journal of Functional Programming, 1(2), 125–154.
• Barendregt, H. P. (1984). The Lambda Calculus: Its Syntax and Semantics. North-Holland.
• Barendregt, H., Dekkers, W. y Statman, R. (2013). Lambda Calculus with Types. Cambridge University Press.
• Bertot, Y. y Castéran, P. (2013). Interactive Theorem Proving and Program Development: Coq'Art. Springer.
• Carneiro, M. (2019). The type theory of Lean [Tesis de maestría]. Carnegie Mellon University.
• Church, A. (1936). An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2), 345–363.
• Coquand, T. y Huet, G. (1988). The Calculus of Constructions. Information and Computation, 76(2–3), 95–120.
• Coquand, T. y Paulin, C. (1990). Inductively defined types. En COLOG-88 (LNCS 417, pp. 50–66). Springer.
• FormalizedFormalLogic (2024). Foundation: Formalizing mathematical logic in Lean 4 [Biblioteca de Lean 4]. https://github.com/FormalizedFormalLogic/Foundation
• Geuvers, H. (2001). Induction is not derivable in second order dependent type theory. En Typed Lambda Calculi and Applications (LNCS 2044, pp. 166–181). Springer.
• Gonthier, G. (2008). Formal proof — the four-color theorem. Notices of the AMS, 55(11), 1382–1393.
• Hoare, C. A. R. (1961). Algorithm 64: Quicksort. Communications of the ACM, 4(7), 321.
• Hoare, C. A. R. (1962). Quicksort. The Computer Journal, 5(1), 10–16.
• Hudak, P., Hughes, J., Peyton Jones, S. y Wadler, P. (2007). A history of Haskell: Being lazy with class. En Proceedings of HOPL III (pp. 12-1–12-55). ACM.
• Huth, M. y Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems (2.ª ed.). Cambridge University Press.
• Kalmár, L. (1935). Über die Axiomatisierbarkeit des Aussagenkalküls. Acta Scientiarum Mathematicarum, 7, 222–243.
• Leroy, X. (2023). The CompCert C verified compiler: Documentation and user’s manual. Inria.
• Nederpelt, R. y Geuvers, H. (2014). Type Theory and Formal Proof: An Introduction. Cambridge University Press.
• Paulin-Mohring, C. (1993). Inductive definitions in the system Coq: Rules and properties. En Typed Lambda Calculi and Applications (LNCS 664, pp. 328–345). Springer.
• Sørensen, M. H. y Urzyczyn, P. (2006). Lectures on the Curry–Howard Isomorphism. Elsevier.
• Stansifer, R. (2001). Completeness as a program. Notas de curso, Florida Institute of Technology.
• Wadler, P. (2015). Propositions as types. Communications of the ACM, 58(12), 75–84.