CSC501 Homepage

Programming Language Semantics

Fall 2018


Dr. Lutz Hamel
Tyler Hall Rm 251
Office hours: Monday/Wednesday 11-noon


As processors become faster and computers become more interconnected our software systems become more complex to take advantage of these additional computational resources. This trend is also reflected in our programming languages where new features are evolving to deal with the distributed nature of our computational resources and to deal with the architecture of modern processors (e.g. multi-core processors). With this added complexity it is often difficult to establish that a program or programming language system behaves correctly. One way to approach the correctness of programs and language systems is to use formal methods. In this approach we usually construct a model of the software system or programming language system in a rigorous mathematical formalisms such as first-order logic and then prove that the model exhibits the intended (correct) behavior.

The application of formal methods applied to programming languages has two interesting points:

The latter is interesting in its own right from a language design perspective; once we have a formal description of every feature of a programming language we can study how features interact in a rigorous way; we can study if a particular feature has the intended behavior under special circumstances. Furthermore, we can achieve this without having to go through the trouble of building an actual implementation of the language. Thus, besides being able to establish correctness of software systems, in the case of programming languages formal methods are also a good design tool.

Formal methods applied to programming languages come in many different flavors under many different names such as "axiomatic semantics", "operational semantics", "denotational semantics", etc. each name indicating a different mathematical formalisms used to model a programming language. Collectively the approach of applying formal methods to programming languages is referred to as programming language semantics.

In this course we will use two flavors of first-order logic as our formal systems. The first approach uses first-order logic in conjunction with a deduction system called natural deduction and is usually referred to as natural semantics. The second approach uses a specialized version of first-order logic called Horn Clause Logic together with a deduction system called the resolution principle. The advantage of this latter approach is that the deductions in this logic are machine executable. Being able to execute deductions mechanically allows us to complete much more complex proofs than otherwise possible since the machine will handle many of the proof details. This approach is often referred to a executable operational semantics.

The aim of this course is to familiarize you with the basic techniques of applying formal methods to programming languages. This includes constructing models for programming languages and use these models to prove properties such as correctness and equivalence of programs. We will look at all major programming language constructs including assignments, loops, type systems, and procedure calls together with their models. Since many of our models are executable, we can test and prove properties of non-trivial programs.

Documents of Interest:

Literature Pointers

NOTE: email submissions are not acceptable for assignments.