Software Foundations

1 Course Unit

This course introduces basic concepts and techniques in the foundational study of programming languages. The central theme is the view of programs and programming languages as mathematical objects for which precise claims may be made and proved. Particular topics include operational techniques for formal definition of language features, type systems and type safety properties, polymorphism, constructive logic, and the Coq proof assistant. This course is appropriate as an upper-level undergraduate CIS elective. Undergraduates who have satisfied the prerequisites are welcome to enroll. There are no formal prerequisites, but students should know how to program at the level of a couple of undergrad courses and have developed some "mathematical maturity" (through two or more undergraduate math courses, including at least one involving rigorous proofs); a course in functional programming or compilers may also be helpful. Fall or Spring 1 Course Unit