In this post, I outline a proposed dependent type theory for the binderless SK calculus. I link the project’s textbook, where you can learn more about my efforts.