CS 611

OverviewThis course covers formal techniques for describing computation and compilation. By developing a framework for precisely characterizing programming languages, we obtain a more general understanding of programming languages, program specification, and proof theory. We study both how programs compute (operational semantics) and what programs compute (denotational semantics). We also examine type systems and other ways to usefully restrict the set of legal programs. Using these techniques, we can prove important properties: for example, that a programming language has a sound type system, that a compiler preserves type safety, or that an optimizer does not introduce bugs. The methods involved have increasing importance for all of computer science. 
Announcements(12/20) Final exams and solutions can be picked up from Esha in Upson 4119. Mean = 73, Median = 79, s = 14. Enjoy the holidays! 
Administration

Resources
