Course Description
This course will cover programming languagebased techniques which apply to software development, software verification, models of computation, and logical foundations of mathematics. Related subtopics include programming language design, compiler implementation, program analysis, software security, and higherorder 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:152:30pm, ROWELL 118
Instructor: David Darais
Office Hours: Thursdays, 3:305:30pm, Votey 319
TAs: John Ring, Alex Grech, Ramy Koudsi
Office Hours: John: Fridays 10am12pm, Farrell 200C. Alex: Fridays 24pm, Perkins 100. Ramy: Tuesdays 68pm, 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:
Git and Version Control:
LaTeX and 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 for assignments. Using LaTeX will be required for the final project.
Policies
Grades: Your grade for the course will be calculated as follows: 60% Assignments (6 assignments at 10% each assignment), 20% Midterm Exam, and 20% Final Project. The last assignment is a final project checkpoint. In total, the final project (checkpoint assignment + final submission) is 30% of your final grade.
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. There is no final exam, 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 extensionit 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 highlevel 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 highlevel 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 1020 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
 Homework 1 (LaTeX Source) (Solution)

Homework 2 (.pdf)
(Solution)
Homework 2 Code (.ml) (Solution) 
Homework 3 (.pdf)
(Solution)
Homework 3 Code (.zip) (Solution) 
Homework 4 (v1.1) (.pdf)
Homework 4 Code (.zip) (Solution) 
Homework 5 (v1.0) (.pdf)
Homework 5 Code (.zip) (Solution)  Final ProjectProposal (Due Friday, April 20)
 Final ProjectCheckpoint (Due Friday, April 27)
 Final ProjectPresentation Draft (Due Monday, April 30)
 Final ProjectPresentation (Inclass Tuesday, May 01 and Thursday, May 03)
 Final ProjectFinal Submission (Due Monday, May 07)
Extra Credit
 Extra Credit 1 (Worth 5% bump to grade; Due Wednesday March 21; Extension to 11:59pm, Sunday, March 25.)
Resources
 OCaml Intro 1 (Jan 23)
 OCaml Intro 2 (Feb 06)
 Type Checking in OCaml 1 (Feb 15)
 Type Checking in OCaml 2 (Feb 15)
 Functional Programming 1 (In Class) (Feb 27)
 Functional Programming 1 (My Notes) (Feb 27)
 Midterm Review (v1.8) (Mar 02; updated Mar 07)
 Midterm Solution (Mar 21)
 Functional Programming 2 and References (In Class) (Mar 21)
 Functional Programming 2 and References (My Notes) (Mar 21)
 Programming with Quantifiers (Mar 29)
 ListMap in Java (Mar 29)
 Software Verification Intro Tutorial (Apr 30)
Small Group Assignments
For homework 4 and 5 only you will be allowed to work in groups of size 1–2 (independently or in pairs). You may submit a single solution to the assignment, as well as a writeup of how the group arrived at the final solution. There will be more detailed instructions about how to submit groupwork in the assignment writeup.
Final Group Project
We will have a final project instead of a final exam. You will be allowed to work in groups of size 1–4 for the final project, however I will expect a larger amount of work to be completed as group size increases. See the final project page for more details.
Schedule
Date  Topic  Homework 

Tue, Jan 16  ✓ Introduction; Chapter 1  
Thu, Jan 18  ✓ Chapters 23  Homework 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 5  Homework 2 Posted Feb 04 
Tue, Feb 06  ✓ OCaml Intro 2 (See Resources)  
Thu, Feb 08  ✓ Chapter 8  Homework 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 Feb 18 
Tue, Feb 20  ✓ Chapter 11  
Thu, Feb 22  ✓ Chapter 11  Homework 3 Due Monday, Feb 26, 11:59pm 
Tue, Feb 27  ✓ Functional Programming 1 (See Resources)  
Thu, Mar 01  ✓ Midterm Review (See Resources)  
Tue, Mar 06  Town Meeting Day Recess  
Thu, Mar 08  ✓ Midterm Exam (See Resources for Solutions)  
Tue, Mar 13  Spring Recess  
Thu, Mar 16  Spring Recess  
Tue, Mar 20  ✓ Functional Programming 2 and References (See Resources)  
Thu, Mar 22  ✓ Chapter 13  Homework 4 Posted Sunday, March 25 
Tue, Mar 27  ✓ Chapter 13  
Thu, Mar 29  ✓ Programming with Quantifiers (See Resources)  Homework 4 Due Monday, Apr 02, 11:59pm 
Tue, Apr 03  ✓ Chapter 23 & 24 Dynamics  
Thu, Apr 05  ✓ Chapter 23 Statics  Homework 5 + Project Proposal Info Posted Sunday, April 08 + Monday, April 09 
Tue, Apr 10  ✓ Chapter 24 Statics  
Thu, Apr 12  Class Canceled  Homework 5 Due Monday, Apr 16, 11:59pm 
Tue, Apr 17  ✓ Git and LaTeX  
Thu, Apr 19  ✓ LaTeX, Makefiles, and intro to Software Verification  Project Writeup Due Friday, Apr 20, 11:59pm (No Extensions) 
Tue, Apr 24  ✓ Coq Tutorial  
Thu, Apr 26  Class Canceled (Final Project Office Hours)  Project Checkpoint Due Friday, April 27, 11:59pm (No Extensions) Project Draft Presentation Due Monday, April 30, 11:59pm (No Extensions) 
Tue, May 01  Project Presentations  
Thu, May 03  Project Presentations  Full Project Due Monday, May 07, 11:59pm (No Extensions) 
Last updated April 30, 2018