Language-based security relies on techniques from programming languages such as automated program analysis, type checking, certifying compilers to enforce security policies in networked computing environments. This course looks at advanced principles of programming languages and verification techniques. In particular, we discuss mathematical foundations such as type systems, lambda calculus and proof theory, underlying the theory and practice of functional programming, as well as representation and verification of safety and security policies. We will particular attention to the formalization of the meta-theory about programing languages.
Prerequisites:: This course is for graduate students and advanced undergraduates who wish to pursue research in programming languages or security. It will assume a basic knowledge of programming language semantics (at the level of COMP-302) and considerable mathematical maturity (COMP-330 and MATH-240).