CS 7480: Special Topics in PL:
Formal Security for Cryptography
Background Materials
Programming Language Foundations
An understanding of the Simply Typed Lambda Calculus (STLC) will
be useful for those papers which use the language of PL.
To read up on this, I recommend Chapters 1-3, 5, 8-9, and 11 of Benjamin Pierce's textbook
Types and Programming Languages.
Cryptographic Background
This class will mostly deal with "ordinary" cryptography, including symmetric encryption schemes, digital signatures,
and hash functions. As a reference, you can take a look at the below resources:
Verification
This class will touch upon formal verification, which uses
software tools to conduct mathematically precise proofs about programs.
If you haven't had experience with formal verification, I recommend taking a look below:
- SAT/SMT-based tools. These tools, such as Dafny,
analyze programs by exporting verification conditions to automatic theorem provers,
such as Z3.
- In contrast, type theory-based tools such as Coq or Lean
present general-purpose, foundational tools for mathematical reasoning, which can then be used to analyze programs
(among other tasks).