CSC501 Homepage
Programming Language Semantics
Fall 2018
Instructor:
Dr. Lutz
Hamel
Tyler Hall Rm 251
Office hours: Monday/Wednesday 11-noon
email: lutzhamel@uri.edu
Description:
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:
- We can formally establish that a programming language implementation is
correct.
- We obtain a mathematically precise description of the behavior of every
feature in the programming language under consideration.
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.
Assignments: