This class will study current research topics in cryptography. In this edition, we will focus on the applied side of cryptography, i.e., we will look at the research surrounding cryptographic methods that are either currently in use, or that are candidates for future deployment. We will adopt a rigorous lens, learning to reason formally about security requirements, and whether these goals are achieved.
This course will examine the close connection between formal logic, computation, and programming languages. The two primary areas of investigation will be (1) various systems of formal logic and their connection to different type systems via the Curry-Howard Correspondence; and (2) various fragments of first-order logic and their connection to logic programming languages. The class will involve both understanding the theory behind these connections and implementing these ideas in practice. A basic knowledge of first-order logic is assumed, but a deep background in logic is not required.