CPSC 629: Deductive Systems

 

Instructor: Carsten Schürmann
Department of Computer Science
Yale University
Time: TTh 4:00-5:15
Room: AKW 500

  Home
  Schedule
  Handouts
  Assignments
  Projects
  Links
 
  

News

Assignment 4 is out.

Twelf 1.2 is now installed on all zoo machines. Simply add

(load "/usr/local/twelf/emacs/twelf-init.el")

to your .emacs file.

To install Twelf on your machine, visit the Twelf homepage http://www.twelf.org. Version 1.2 of Twelf is sufficient.

Abstract

We explore the theory of programming languages and the design of logics using deductive systems. In particular, we discuss how to specify, implement, and verify properties of functional and logic programming languages.

The deductive approach to the specification of programming languages has become standard practice, and one of the goals of this course is to provide good working knowledge of how to engineer language descriptions, how to implement and experiment with related algorithms such as operational semantics, and how to verify properties about the design. Throughout this course we will use the Twelf system as a uniform meta-language in which we can express specification and implementation, and meta-theory of the object languages we are considering.

Grades

Students can take this class for credit. In the first half of the course we will have homework assignments, which are being substituted by project work in the second half of the course. The final grade is computed as:
grade = avg(avg(homeworks), project)

Office Hours

My new office hours are Tuesday and Thursday 2:30-4:00 or by appointment.