Welcome to CSCI 5535 Fall 2021 edition! The objective of this course is to study the mathematical foundations of computer programs and programming languages. To understand what we mean by “mathematical foundations”, let’s think back to a familiar concept from high school mathematics. Recall that the equations \(3x+2y-1 = 0\) and \(3y-2x-2 = 0\) describe two straight lines on a Cartesian plane. If you were to plot these lines, you’d see that these lines look quite different; indeed they are literally orthogonal. However, if I were to ask you to find their slopes, or to tell me where they intersect the axes, your approach is likely going to be the same for both the lines. You would treat them as but different instantiations of the linear equation \(ax + by + c = 0\) and thereafter use same mathematics to reason about both. Now consider the equations \(y = 3x^2+2x-1\) and \(y = 2x-1\). This time, not only do the plots of the equations look very different, but the equations themselves are fundamentally different. Using their general forms we can even argue that the former – a quadratic equation is more general or more expressive than the latter – a linear equation.

Now let’s extend this analogy to programs and programming languages. A randomly chosen C++ program likely looks a lot different from a Java program. But are they both fundamentally different? If I were to ask you to show that both C++ and Java programs compute the Fibonacci function, do you need fundamentally different techniques to prove the same? Or is it possible to treat them as just different instantiations of a general form amenable to uniform reasoning? Wouldn’t it be great if there exists a formal mathematics to reason about computer programs that would let us categorically answer these questions?

Why, there is such a mathematics! The formal study of computer programs as mathematical objects predates the invention of the modern computer itself, and continues to this day under the aegis of Programming Languages and Formal Methods research. This course covers several foundational ideas and mathematical techniques that have resulted from this effort. In particular, we are going to study the mathematical abstractions of computer programs that let us understand the fundamental differences among different programming styles and languages. We shall develop the reasoning calculi that let us categorically prove or refute various kinds of assertions about programs, for instance that a program computes the Fibonacci function. We are going to see how the concept of a “proof” can be defined to such a degree of precision that a machine can check if the proof we write is correct or incorrect. In fact we go so far as to only consider such mechanized proofs as real proofs in this course. And whats more, we shall also learn proof automation techniques that let us program a machine to generate a proof rather than just check it! See the lecture schedule to know what else is in store.

Classroom and Office Hours

• Instructor: Gowtham Kaki.
• Where: ECCS 1B14
• When: M,W,F 3:00 - 3:50 PM
• Zoom: https://cuboulder.zoom.us/j/95381898612. Email me for the passcode.
• Office Hours: On Piazza or by appointment.
• Canvas: https://canvas.colorado.edu/courses/77068

Textbook

• We are largely going to use Volume 1 (Logical Foundations) and Volume 2 (Programming Language Foundations) of Pierce et al’s Software Foundations course notes.
• We will refer to Chlipala’s Certified Programming With Dependent Types occasionally.
• Pierce’s Types and Programming Languages is a recommended reading. This book is available for checkout at CU Libraries.

Evaluation Components

Item	Nos.	Weight (%)
Homeworks	8 of 10	40
Mid-term	1	20
Course Project	1	20
Final	1	20