Overview
Meet: Friday 10:10-11:00 in Upson 315
Pre-requisite: Advanced PL CS6110
Credits: 1 or 2
Course Staff
Professor Robert Constable, Instructor
4147 Upson Hall
email: rc at cs dot cornell dot edu
Dr. Vincent Rahli, Assisting
email: vincent dot rahli at gmail dot com
Description
PL Lab is a new course offered in Spring 2012, meeting on Friday mornings.
This course assumes material from CS6110, Advanced Programming Languages. The course will examine applications programming language concepts in other domains including domain specific languages, programming logics, program verification systems, and logical programming environments. The course will also present applications of formal methods to the design of programming languages and to the formal verification of aspects of their implementation. We will use the ML family of programming languages and perhaps the Scheme/Lisp family to illustrate the concepts and methods.
Topics
- domain specific languages
- programming logics
- program verification systems
- logical programming environments
- applications of formal methods
Background Reading
- A Basis for a Mathematical Theory of Computation, John McCarthy Computer Programming and Formal Systems. eds P. Braffort, D. Hirschberg. North-Holland, 1963 (Amsterdam), pp. 33-70.
- Term Rewriting Systems, J.W. Klop. Handbook of Logic in Computer Science. eds S. Abramsky, D. Gabby, T.S. Malbaum. Clarendon Press, 1992 (Oxford), pp. 1-116.
- Lambda Calculi with Types, H.P. Barendregt Handbook of Logic in Computer Science ibid pp. 117-309.
(193 pages, a small book in itself)
- Compiling with Continuations Andrew W. Appel. Cambridge Univ. Press, 1992 (Cambridge).
Related Textbooks
- Types in Programming Languages Benjamin C. Pierce (Benli). MIT Press, 2002 (Cambridge).
Available online with access through the Cornell network (or using VPN) http://library.books24x7.com/toc.aspx?bookid=3447
- Foundations for Programming Languages John C. Mitchell. MIT Press 1996 (Cambridge).
- Type Theory and Functional Programming Simon Thompson. Addison-Wesley, 1991 (NY).
- The Formal Semantics of Programming Languages Glynn Winskel. MIT Press, 1994 (Cambridge).
- Semantics of Programming Languages Carl A. Gunter. MIT Press, 1992 (Cambridge).
- Constructive Foundations for Functional Languages Raymond Turner, McGraw Hill, 1991 (New York).
Other Related Textbooks
- Theory of Computation Dexter C. Kozen. Springer, 2006 (London).
- Automata and Computability Dexter C. Kozen. Springer, 1997 (New York).
- Introduction to Metamathematics Stephen C. Kleene. D. van Nostrand, 1952 reprinted.