Announcements
- Students who are not enrolled but are interested in joining the course should fill out this form: https://docs.google.com/forms/d/e/1FAIpQLSfkQgG40cwUsgBx8Dhx8vsZjQU4T-f81Qm_se5JgF8lq3mnwA/viewform?usp=header
- Lecture will be held in Gates 114 and also accessible via Zoom. The Zoom link will be available on CMSX.
- Each student in this course is expected to abide by the Cornell University Code of Academic Integrity. Any work submitted by a student in this course for academic credit must be the student’s own work.
- These web pages are still under development.
Overview
Programming languages are a fundamental part of computer science. This course introduces the formal tools needed to describe precisely what a program means. These tools help us answer many useful questions about program analyses and transformations, such as:
- Is this program correct?
- Will this program encounter a run-time type error?
- Is one program indistinguishable from another?
- Is this optimization a safe program transformation?
- Does this program compute the intended result? Does it leak information?
- Is this compiler translation correct?
- Can source language A be translated into target language B?
- Different styles of dynamic semantics, including operational, axiomatic, and denotational semantics
- Static semantics, especially type systems
- Proofs by induction on derivations and structure
- A formal treatment of important programming language features such as functions, laziness, exceptions, continuations, modules, type polymorphism, objects and classes.
Course Information
Time & Place
Lecture:
- Monday, Wednesday, and Friday, 10:10-11:00am, location TBA
You are expected to attend all lectures.
Course Staff
Placeholder for staff
Prerequisites
Enrollment limited to: graduate students or permission of instructor. Programming experience and mathematical maturity is required.
Texts
You are required to read the course notes posted on the web site. These will often contain more detail than what was presented in lecture.
Ed
We will be using Ed as an online discussion forum. You are encouraged to post any questions you might have about the course material. The course staff monitor the forum fairly closely and you will usually get a quick response. If you know the answer to a question, you are encouraged to post it, but please avoid giving away any hints on the homework or posting any part of a solution—this is considered a violation of academic integrity.
By default, your posts are visible to the course staff and other students, and you should prefer this mode so that others can benefit from your question and the answer. However, you can post privately so that only the course staff can see your question, and you should do so if your post might reveal information about a solution to a homework problem. If you post privately, we reserve the right to make your post public if we think the class will benefit. You can also post anonymously if you wish not to reveal your identity.
The discussion forum is the most effective way to communicate with the staff and is the preferred mode of interaction. Please reserve email for urgent or confidential matters. Free-ranging technical discussions are especially encouraged. Broadcast messages from the course staff to students will be sent using Ed and all course announcements will be posted there, so check in often.
CMSX
We will be using the course management system CMSX for managing assignments, exams, and grades. Everyone who preregistered for the course should be entered, but if you did not preregister, you are probably missing. Please login here and check whether you exist. There will be a list of courses you are registered for, and CS 6110 should be one of them. If not, please send your full name and Cornell NetID to the course staff so you can be registered.
You can check your grades, submit homework, and request regrades in CMSX. Please check your grades regularly to make sure we are recording things properly. The system also provides some grading statistics. There is a help page with instructions.
Please do not repost course materials released on CMS publicly. These materials are intellectual property and are meant for participants in the course. They are not free to the public.
Announcements and Handouts
Announcements will be posted to Ed. Homework and exam solutions will be available in CMS. Check frequently for new postings.
Assignments & Exams
Unless otherwise specified, assignments may be turned in late with a penalty that starts at 5% and increases by 10% per day up to the late submission deadline on CMSX. Extensions may be granted in case of illness or other acceptable excuse; please contact the course instructor.
There will be a 1½-hour evening prelim and a 2½-hour final exam. Please check the schedule page for times and locations.
Your final grade will be based on your assignment and exam scores according to the following weights:
Participation | 3% | |
Assignments | 45% | |
Assignment 1 | 5% | |
Assignment 2 | 6% | |
Assignment 3 | 6% | |
Assignment 4 | 8% | |
Assignment 5 | 8% | |
Assignment 6 | 12% | |
Prelim | 22% | |
Final | 30% |
Participation will be assessed based on attendance and participation in class, participation in Ed discussions, and pop quizzes given in class (usually right at the beginning!)
Scores will be averaged by computing a weighted quadratic mean, which means that unrepresentatively low scores (such as missing assignments) will have less weight.
Regrades
Graded homework will be available on CMS. Graded exams will be available in the handback room, 216 Gates.
Homework regrade requests can be submitted electronically in CMS. Exam regrades should be handwritten and submitted to the course staff. Graded exams will be available in the handback room in Gates 216. Please include a description of the grading error with your regrade request.
Academic Integrity
Each student in this course is expected to abide by the Cornell University Code of Academic Integrity. Any work submitted by a student in this course for academic credit must be the student’s own work.
The utmost level of academic integrity is expected of all students. Under no circumstances may you submit work done with or by someone else under your own name or share detailed proofs or code with anyone else except your partner. However, discussions about general techniques or the requirements of the assignment are permissible.
You must cite all sources, including Internet sources. You must acknowledge by name anyone whom you consulted (excluding course staff). You may not give nor receive assistance from anyone else during an exam. You may not give any hints or post any material that might be part of a solution publicly on Ed. If your question necessarily includes such material, post privately.
If you are unsure about what is permissible and what is not, please ask.
Academic Integrity Resources:
- • Cornell University Code of Academic Integrity
- • Computer Science Department Code of Academic Integrity
- • Explanation of AI Proceedings
Special Needs
We will provide appropriate accommodation for students with special needs or disabilities. Requests for accommodation are to be made during the first three weeks of the semester and must be accompanied by official documentation. Please register with Student Disability Services in 110 Ho Plaza (Cornell Health Building), Level 5 to document your eligibility.
Course Schedule
Placeholder for schedule
Resources
Course notes
Course notes for individual lectures and recitations can be found on the course schedule.
Useful textbooks
The following books are recommended but not required:
- Types and Programming Languages: Benjamin Pierce
- Formal Semantics of Programming Languages, Glynn Winskel
Some other useful texts that provide a different perspective or more depth in some areas are:
- Programming Languages: Theory and Practice, by Robert Harper (online draft)
- Foundations for Programming Languages, by John Mitchell
- Semantics for Programming Languages, by Carl Gunter
- Basic Category Theory for Computer Scientists, by Benjamin Pierce
Online resources for OCaml:
- OCaml home page
- OCaml support for emacs and vim
- Objective CAML Tutorial
- Introduction to the Objective Caml Programming Language, by Jason Hickey (online version)
- F#, a language similar to OCaml. You can use the Visual Studio IDE to write and debug F# programs.
- Comparison of SML and OCaml, by Andreas Rossberg.
- ledit, a tool to provide emacs-like editing (and history) to the OCaml toplevel. (Info on how to use ledit, and other tips for using the toplevel, here.)
Other useful code
Assignments
All source code will be available on CMS.