Hi! I’m an undergraduate student at the University of Texas at Dallas. I recently started using Coq, and more recently got interested in Combinatory Logic.
To feed my enthusiasm, I’ve started implementing definitions and proofs from the English translation of “Grundlagen der kombinatorischen Logik,” Haskell Curry’s 1930 PhD thesis in which the BCKW combinator calculus system is proposed. I’ve only just started, but I’m having a blast: GitHub - CharlesAverill/HCLT: A Coq implementation of "Foundations of Combinatory Logic," the 1930 Ph.D. thesis written by Haskell Curry
I would greatly appreciate any feedback the community might have on my implementations or proof structures. Thank you!