Tyler Hall Rm 251

Office hours: Monday/Wednesday 11-noon

email: lutzhamel@uri.edu

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.

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.

- Wikipedia's take on the topic
- Rewriting Tutorial by N. Dershowitz
- Natural Semantics by Gilles Kahn
- Structured Operational Semantics by Gordon Plotkin
- Denotational Semantics by David Schmidt (the figures for chapter 1 can be found here)
- Benjamin Pierce's Great Works in Programming Languages
- Book: Semantics with Applications (a primer)
- Book: The Formal Semantics of Programming Languages (a classic, mathematically demanding)

NOTE: email submissions are not acceptable for assignments.

- Assignment #1
- Assignment #2
- Assignment #3
- Assignment #4. 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 Prolog facts. Please upload a copy of your programs together with a log that shows that the programs execute.
- Assignment #5
- Assignment #6