CSC501 Homepage
Programming Language Semantics
Fall 2009
Official Statement on Illness Due to the H1N1 Flu
The H1N1 Flu Pandemic may impact classes this semester. If any of us develop
flu-like symptoms, we are being advised to stay home until the fever has
subsided for 24 hours. So, if you exhibit such symptoms, please do not come to
class. Notify me using hamel@cs.uri.edu of your status, and we will communicate
through the medium we have established for the class. We will work together to
ensure that course instruction and work is completed for the semester.
The Centers for Disease Control and Prevention have posted simple methods to
avoid transmission of illness. These include: covering your mouth and nose with
a tissue when coughing or sneezing; frequently washing your hands to protect
from germs; avoiding touching your eyes, nose and mouth; and staying home when
you are sick. For more information, please view http://www.cdc.gov/flu/protect/habits.
htm . URI information on the H1N1 will be posted on the URI website at http://www.uri.edu/news/H1N1 , with links to
the http://www.cdc.gov site.
(End of official statement)
Description:
Formal semantics of programming languages is concerned with the rigorous, i.e. mathematical,
description of the meaning of programming languages. In this mathematical approach to programming
languages we are concerned with constructing models of programming languages that allow us to prove
basic properties of the programming languages under consideration.
In this course will primarily focus on two approaches to formal semantics: (a) operational
semantics (b) the denotational approach to programming language semantics. Both approaches are well
established. The operational semantics we will study is based on natural deduction. After introducing
the mathematical concepts we will proceed to make the semantics specifications machine executable
using Prolog. We will investigate concepts such as program equivalence, program correctness, and
provably correct translation.
Perhaps the most well known denotational semantics is the approach developed by John
McCarthy and then refined by Christopher Strachey based on functions, functional composition, and
domain theory. At the core of this approach is the lambda calculus.
The aim of this course is to familiarize you with the basic techniques of specifying semantics
for programming language constructs and use these formalisms to prove properties of the constructs in
question. We will look at all major programming language constructs including assignments, loops,
and procedure calls together with their semantics. We will develop models for both imperative and
functional programming languages. Since our specifications are executable, we can test and prove
properties of non-trivial programs.
Announcements:
[11/16/09]Important:
It is clear that laptops and other electronic communication equipment represent
a huge distraction during lectures.
Therefore, as of now, laptops, iphones, and any other electronic communication
equipment are no longer allowed during class. If you want personal access to
the class notes slides during class you will need to bring hardcopies with
you.
Exceptions to this new policy are only granted with official documentation.
[11/19/09] Please read chapters 2,3, and 4 (4.1 and 4.2 only) in David Schmidt's book.
[11/19/09] Posted assignment #7
[11/13/09] Posted assignment #6 (translation specifcations contained in a zip file)
[11/3/09] Posted solution to assignment #4
[11/3/09] *** Midterm *** is available here. It is due in
class 11/10/09
[10/30/09] Posted assignment #5
[10/26/09] Hints for assignment #4 problem 2: The proof should proceed via case analysis on a. All of
your assumptions should be made in the semantic domain.
[10/20/09] Posted assignment #4
[10/15/09] Added section to 'Documents of Interest' called 'Specifications & Proof Scores'. Here
you will find all the specifications we looked at in class and associated proof scores.
[10/10/09] Posted solutions for assignment #2
[10/6/09] Posted assignment #3
[10/6/09] Read the Prolog tutorial
by Steve Harlow up to and including section 3.1 (the tutorial is also available
on the Prolog resource page)
[10/5/09] Posetd a new version of assignment #2. Question 3 had a typo, the inequality should
have read L(b) <= O(b) + 1. I also tried to make the question 4c less ambiguous.
[10/1/09] Posted assignment #2
[10/1/09] Posted solutions to assignment #1 (also available as a link below)
[9/24/09] Posted Assignment #1
[9/12/09] I have rewritten the intro slides and added some clarification on implication
[9/1/09] You should go to the online grade book
and sign up for an account, your access code is engrade-csc501fall2009-nnnn where nnnn is your
student ID number.
[9/1/09] Welcome!
Documents of Interest:
Literature Pointers
NOTE: email submissions are not
acceptable for assignments.
Assignments:
- Assignment #1 - due on Tuesday 9/29 in class.
- Assignment #2 - due on Tuesday 10/6 in class.
- Assignment #3 - due on Tuesday 10/13 in class. 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 hand in a hardcopy of your programs together with a log that shows that the programs
execute.
- Assignment #4 - due on Tuesday 10/27 in class.
- Assignment #5 - due on Tuesday 11/3 in class.
- Assignment #6 - due on Tuesday 11/17 in class.
- Assignment #7 - Due Tuesday 11/14 in class: prove the correctness of the translation of
Aexp into stack machine code.
Instructor:
Dr. Lutz
Hamel
Tyler Hall, Room 251
Office hours: Tu 2:30-3:30 W 11am-12pm
email: hamel@cs.uri.edu