Course Description

This course will cover programming language-based techniques which apply to software development, software verification, models of computation, and logical foundations of mathematics. Related sub-topics include programming language design, compiler implementation, program analysis, software security, and higher-order logic. Course topics will be approached from the perspective of type theory. Coursework is intended to be a 50/50 split between exercising mathematical concepts and implementing algorithms.

Prerequisites: CS 124 and CS 125.

Administration

Lecture: Tuesdays and Thursdays, 1:15--2:30pm, ROWELL 118

Instructor: David Darais
Office Hours: Thursdays, 3:30--5:30pm, Votey 319

TAs: John Ring, Alex Grech, Ramy Koudsi
Office Hours: John: Fridays 10am--12pm, Farrell 200C. Alex: Fridays 2--4pm, Perkins 100. Ramy: Tuesdays 6--8pm, CS Conference Room.

Course Piazza: CS 225: Programming Languages
Course announcements and discussion will take place on Piazza exclusively.

Textbook

The textbook we will use for this course is Pierce's Types and Programming Languages. It is highly recommended you obtain a personal copy to use throughout the course. Homework problems will be drawn directly from this textbook, and the exams will be open textbook in addition to only one page of other notes.

Software Tools

Programming Language: Many of the assignments will have a programming component. We will use the OCaml programming language for these assignments. For the first assignment you will be required to successfully set up and configure OCaml on either your personal machine or a computer lab machine. We will use OCaml version 4.06.0 for the entirety of the course.

Instructions for setting up OCaml

OCaml Resources:

Formal Writing: Many of the assignments will have a written mathematics component. If you want to write your solutions on a computer, I recommend using the LaTeX typesetting system. However, using LaTeX is not required.

Policies

Grades: Your grade for the course will be calculated as follows: 60% Assignments, 20% Midterm Exam, and 20% Final Exam.

Attendance: Attendance is not mandatory but will be rewarded. Attendance will be taken every class. Students who miss no more three classes will receive an automatic 5% extra credit to their final grade.

Exams: There will be one midterm on March 08, and one final exam on May 03. Each exam will be open textbook, meaning you may reference the Types and Programming Languages text during exams. You will also be allowed one physical page (8 1/2" x 11") of notes for each exam. The final exam will only cover material covered after the first midterm, and is intended to be the same difficulty as the midterm. The final exam will take place during the last class, and this course will conclude before the University's exam period.

Late Work: Each assignment will typically be released on a Sunday night, and due a week from the following Monday at 11:59pm. I will automatically grant a deadline extension up to that Wednesday at 11:59pm. You do not need to email me or any TAs to receive the extension---it is automatic. There is no penalty for submitting work before Wednesday at 11:59pm. Work will not be accepted after Wednesday at 11:59pm except in the case of personal emergencies.

Collaboration: Collaboration on the high-level ideas and approach on assignments is encouraged. Copying someone else's work is not allowed. Any collaboration, even at a high level, must be declared when you submit your assignment. Every assignment must include a collaboration statement. E.g., "I discussed high-level strategies for solving problem 2 and 5 with Alex." Students caught copying work are eligible for immediate failure of the course and disciplinary action by the University. All academic integrity misconduct will be treated according to UVM's Code of Academic Integrity.

Invited Talks: I will give +1% extra credit to your final grade (~10 assignment points) for each faculty candidate talk you attend. You must write 10-20 sentences about what the candidate talked about, and what you found interesting about the presentation. Specifically, you must include (1) the candidate's main research result, and (2) the candidate's proposal for future research. I expect each candidate will have slides indicating these points directly. If they don't, say in your writeup that the speaker wasn't specific regarding these points. You must email me your writeup within 24 hours of the talk to receive credit. See the Piazza announcement for dates, times, locations, and talk titles.

Assignments

Resources

Schedule

Subject to change... E.g., I am considering either replacing or supplementing the final exam with a final project.
DateTopicHomework
Tue, Jan 16✓ Introduction; Chapter 1
Thu, Jan 18✓ Chapters 2--3Homework 1 Posted
Tue, Jan 23✓ Chapter 3
Thu, Jan 25✓ OCaml Intro 1 (See Resources)Homework 1 Due Friday, Jan 26, 11:59pm
Tue, Jan 30✓ Chapter 5
Thu, Feb 01✓ Chapter 5Homework 2 Posted (on Feb 04)
Tue, Feb 06✓ OCaml Intro 2 (See Resources)
Thu, Feb 08✓ Chapter 8Homework 2 Due Monday, Feb 12, 11:59pm
Tue, Feb 13✓ Chapter 9
Thu, Feb 15✓ Type Checking in OCaml 1&2 (See Resources)Homework 3 Posted (on Feb 18)
Tue, Feb 20Chapter 11
Thu, Feb 22More OCamlHomework 3 Due Monday, Feb 26, 11:59pm
Tue, Feb 27Chapters 12
Thu, Mar 01Midterm Review
Tue, Mar 06Town Meeting Day Recess
Thu, Mar 08Midterm Exam
Tue, Mar 13Spring Recess
Thu, Mar 16Spring Recess
Tue, Mar 20Chapters 13--14
Thu, Mar 22Chapters 13--14Homework 4 Posted
Tue, Mar 27Chapters 13--14
Thu, Mar 29Chapters 22--25Homework 4 Due Friday, Mar 30, 11:59pm
Tue, Apr 03Chapters 22--25
Thu, Apr 05Chapters 22--25Homework 5 Posted
Tue, Apr 10Chapters 22--25
Thu, Apr 12Chapters 29--30Homework 5 Due Friday, Apr 13, 11:59pm
Tue, Apr 17Chapters 29--30
Thu, Apr 19Chapters 29--30Homework 6 Posted
Tue, Apr 24Information Flow Types
Thu, Apr 26The Cutting EdgeHomework 6 Due Friday, Apr 27, 11:59pm
Tue, May 01Final Review
Thu, May 03Final Exam

Last updated February 19, 2018