This is an archived page and may be obsolete; the current pages are at

CS 536: Science of Programming

Course Description

We will study how to formally specify how programs execute (operational semantics), how to describe what mathematical functions programs compute (denotational semantics), and how to use logic to characterize properties and invariants of the program execution (axiomatic semantics). Using these specifications, we can prove interesting and relevant properties of programming languages: for example, that a programming language has a sound type system, or that a compiler preserves type safety. These techniques have significant practical utility and are becoming increasingly relevant to other areas of computer science.




Edited March 2006 (html, css checks)