Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
[go: Go Back, main page]

CS256  Spring 2006

Programming Languages and Semantics

Greg Morrisett
Wed & Fri 2:30-4:00pm, Maxwell Dworkin 221

Overview:

This course concerns semantic models of programs and systems and how we use those models to prove properties of programs, protocols, and languages. For example, we look at techniques for proving the input-output equivalence of two programs, or proving that a language is type-safe, or proving that an analysis is sound. Along the way, we will consider how to model advanced linguistic features such as references, closures, objects, exceptions, continuations, threads, and channels.

This year, we're also going to consider how to mechanize some of these models and proofs.  It's relatively easy to mechanize models (this just amounts to writing an interpreter) but it's not so easy to mechanize a proof about that model unless we use some "pure" programming environment for building the models.  We'll consider how two environments (Twelf and Coq) for mechanization. 

Regarding prerequisites, CS152 is probably a good idea.  Preferably, students will have some knowledge and experience working with a functional language, such as Scheme, ML, or Haskell. The more experience with programming in different programming languages, the better. On the theoretical side, we assume a basic proficiency in undergraduate mathematics, logic, and computer science. A basic knowledge of computability (such as Turing machines and recursive functions) and logic (that is, predicate calculus), as well as some mathematical maturity is required.

Grades will be determined by a combination of homeworks and class participation.  The homeworks will consist of a combination of written and programming exercises.  Class participation includes showing up and scribing lectures. 

There is no required text for the course, though the following books provide pieces of the material that we'll be going through.

Tentative Syllabus:


Topic
IMP/Operational Semantics
Introduction to Twelf   (See end for Homework #1)
   See also the Twelf Home page and Wiki.
IMP/Denotational Semantics
IMP/Axiomatic Semantics
Weakest Pre-Conditions, Strongest Post-Conditions and Verification-Conditions
Simply-Typed Lambda Calculus ,
Reduction, Confluence, and Strong Normalization
Some Twelf code.
Denotational and Algebraic Semantics
Exceptions, Stacks, and Continuations
State
Threads, Channels, and Concurrency
Parametric Polymorphism, Type Inference
Pure Type Systems
Recursive Functions and Recursive Types
Subtyping and Bounded Polymorphism
Substructural Typing