Programming Language Semantics
Tyler Hall Rm 251
Office hours: Mon and Wed 10am-11am and by apointment
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
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.
- We can formally establish that a programming language implementation is
- We obtain a mathematically precise description of the behavior of every
feature in the programming language under consideration.
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.
[12/15/11] NOTE: the program in final in problem 3 (a) part 2 should read:
[12/14/11] Posted solutions for assignment #6
[12/7/11] ** Final exam is due on Wednesday 12/21/11 @ noon in my office**
[12/7/11] posted the correctness proofs of loops and functions (see specs)
[12/2/11] Posted homework assignment #6
[11/23/11] Posted midterm solutions.
[11/22/11] Please bring your laptops to class today...we will be doing some correctness proof exercises.
[11/10/11] This time posted the correct version of the the solutions to assignment #5
[11/7/11] Posted solutions to assignment #5
[11/6/11] The midterm is now available. It is due
in class on Tuesday 11/15/11.
[11/1/11] Hint for Assignment #5: when constructing proofs be careful about the
kind of values you are looking at, most likely they are not values per se but
structures that represent values, e.g.
% xis.pl compiled 0.00 sec, 7,792 bytes
% preamble.pl compiled 0.01 sec, 8,920 bytes
% xis.pl compiled 0.00 sec, 148 bytes
% sem.pl compiled 0.01 sec, 15,232 bytes
?- (eq(x,x),s) -->> V.
V = (vx=:=vx).
This is still a valid statement because the structure vx=:=vx represents an actual value.
[10/27/11] Posted assignment #5
[10/20/11] Posted solution for assignment #4
[10/20/11] Posted the prolog specifications, see the specs folder
[10/13/11] posted assignment #4
[10/11/11] posted solutions for assignment #3
[10/5/11] posted assignment #3
[10/5/11] posted solutions for assignment #2
[9/30/11] solutions page is now live
[9/27/11] posted assignment #2
[9/22/11] the online gradebook website is live...email me for the access code if you haven't
[9/19/11] posted assignment #1
[9/7/11] You should go to the online grade book
and sign up for an account (email me for your access code).
Documents of Interest:
NOTE: email submissions are not
acceptable for assignments.
- Assignment #1 - due on Tuesday 9/27 in class.
- Assignment #2 - due on Tuesday 10/4 in class.
- Assignment #3 - due on Tuesday 10/11 in class.
- Assignment #4 - due on Thursday 10/20 in class. Read and do all exercises in the
tutorial up to and
including section 3.1 except exercise 9. For exercise 1 you can assume these
Please hand in a hardcopy of your programs together with a log that shows that the programs
- Assignment #5 - due on Thursday 11/3 in class.
- Assignment #6 - due on Monday 12/12 in my office.