**CS 6110 (Spring 2023)
Advanced Programming Languages** # Logistics - Lectures: **Gates 114**, Mondays, Wednesdays, and Fridays 10:10 AM - 11:00 AM - Questions: [Slack][] (##) Staff Instructor: Alexandra Silva - Web: - Email: - Office hours: Monday 11.15-12.15 in Gates 434 TA: Jacob Wasserstein - Email: - Office hours: Wednesday 12-1 in Gates 434, Friday 11-12 in Rhodes 408 TA: Noah Bertram - Web: - Email: - Office hours: Tuesday 2pm - 3pm on zoom and Thursday 9:30am-10:30am in Rhodes 406 (#) Announcements - 01/22: Welcome to CS 6110! # Syllabus CS 6110 is Cornell's graduate class on programming languages. It represents what we think every CS PhD student should know about the theory and practice underlying programs. It blends formal foundations with real-world applications and connections to other fields in computer science. (##) TL;DR - All course communication will happen on [Slack][]. - Please [sign up][slack-signup] using an @cornell.edu or @cs.cornell.edu email address. - You're responsible for knowing everything that gets posted in #announcements. Please turn on notifications for that channel. - Homework and grading happens on [Gradescope][]. - There will be four two-week homework assignments. - You can work in pairs on homework if you like, in which case you'll write one submission together. - The deadline is always Wednesday night at 11:59pm. There are no points for late work, but please Slack us if you have extenuating circumstances. - There will be one prelim and one final exam. - Both are "take-home" exams. You'll have one week to complete the prelim. - The homework and exams may feel different from other classes, especially undergrad courses. - Expect the assignments to make you try things we haven't done in class. Expect to get stuck and to ask for help. Exams will be less expansive but will still require original thought. - Grading for assignments uses a gold-star system: you get full credit if you do everything reasonably well. - Grading for exams will have a high standard for precision. Because this class is about formalism, little details matter more than the getting the gist right. [gradescope]: https://www.gradescope.com/courses/500972 [finals]: https://registrar.cornell.edu/exams/spring-final-exam-schedule [slack-signup]: https://join.slack.com/t/cs6110sp23/shared_invite/zt-1njeaeddj-1GnrTU5gSC7N1etY~U_DQQ [slack]: https://cs6110sp23.slack.com (##) Organization (###) Announcements and Q&A: Slack We will use a [Slack][] workspace for announcements and communication about the course. (We're using Slack *instead of* Piazza or Ed this semester.) Please [sign up for the Slack instance][slack-signup]. The course staff will post important updates there that you really want to know about! Check often, and be sure to enable notifications for the #announcements channel. You can also ask questions---about lectures, homework, or anything else---on Slack. The #pl channel is for this kind of discussion. The course staff will respond as quickly as possible. If you can answer a question yourself, please do! But be careful not to post answers---if you're not sure whether something is OK to post, contact the course staff privately. You can do that by sending a **direct message** in Slack to Alexandra **and** the TAs. A good post asks a specific question. Here are some examples of bad Slack posts: * "Tell me more about broad topic X." * "Does anyone have any hints for problem Y?" If you need help with a homework problem, for example, be sure to include what you've tried already, exactly where you're stuck, and what you're currently thinking about how to proceed. If you just ask for help without any evidence of effort, we'll punt the question back to you for more details. (###) Assignments: Gradescope You will download homework assignments, upload solutions, and receive grades through [Gradescope][]. Please log in there to see whether you're in the system. If you're not, please send your NetID to the course staff and we'll get you set up. Please, put your name and/or NetID onto your pdf solutions. We might need to print out the documents in order to grade them, so without your name or NetID it becomes difficult to match your work with you! (##) Grading Final grades will be assigned with these proportions: * Assignments: 35% * Preliminary exam: 30% * Final exam: 30% * Participation: 5% There is no algorithm for "curving" grades or any predetermined cutoffs, so we won't be able to answer questions about letter-grade projections. (###) Assignments Assignments are due on Wednesdays at 11:59 PM. See the course schedule. You can work on assignments with a partner; you'll turn in one completed assignment together. You'll turn in assignments via [Gradescope][]. We strongly encourage you to use TeX, but you can also write up answers by hand. If you do, scan your work and upload it as a PDF. It's your responsibility to make sure scans are 100% legible---we won't regrade work that was too hard to read. (###) Gold-Star Grading

We are using a simplified grading scheme for assignments this semester. Our goal is to focus on giving you useful feedback, not on "precisely" scoring every granular facet of a homework problem. There are three possible outcomes: - If you do everything reasonably well, whether you have lots of mistakes or are more or less perfect, you will receive a gold star. Congratulations! - If you do something surprisingly awesome, you will receive a *sparkly* gold star. This is uncommon. - If your work has major gaps or significant misunderstanding, you may receive no stars. This is also uncommon. Earning gold stars on every assignment will achieve an A in the "assignments" category of your course grade. (###) Timeliness Late work will not be accepted and will count for zero points. If you need an extension for extenuating circumstances, please talk to the course staff. (###) Exams There will be a prelim and a final, both in a take-home format. You'll be able to take the exams anywhere within a one-week period. See the course schedule. Makeup exams must be scheduled within the first three weeks of class. Check the schedule now to see if you have a conflict with another class and contact the instructor immediately to reschedule. (###) Participation To get full credit on the 5% of your grade allocated to participation, you just have to do three things: * Drop by Alexandra's office hours sometime in the first two weeks of February to introduce yourself. * Fill out the mid-semester feedback survey. * Fill out the semester-end course evaluation. Free points! (###) The Difficulty You Can Expect This is a PhD-level course, which means the homework and exams can feel very different from undergrad courses. These differences may be surprising, especially if this is one of your first grad classes: * The homework will ask you to do new things *that you have not practiced already during lecture*. This can make the homework feel difficult, and you may even get totally stumped on some problems. This is normal. But it does mean that you should start early and leave time to ask questions. * Problems on exams will feel more familiar and should stretch you somewhat less. On the other hand, they will not be slightly tweaked versions of previous homework problems. Grading on exams will intentionally focus on nitpicky details. Compared to other courses, we will give more weight to "small" mistakes and less weight to getting the general idea right. That's the nature of this course, which is about formalism. Often, the intuitive idea behind a problem is totally obvious! Then, the topic we're working on is 100% about getting the nitty-gritty formal details right so we can prove something beyond a shadow of a doubt. Here's a special message for PhD students: Please try not to worry about your grade. I don't know how to put this delicately, but grades matter less as a PhD student than they did in undergrad. Focus on getting as much PL knowledge as you can out of this course---not on acing every assignment. # Resources (##) OCaml and Functional Programming Programming assignments for this course use the [OCaml][] language. Here are some [instructions for installing OCaml][install]. (In contrast with that guide, I recommend [Homebrew][] on macOS: just type `brew install ocaml`.) [ocaml]: https://ocaml.org [homebrew]: https://brew.sh [install]: https://www.cs.cornell.edu/courses/cs3110/2020sp/install.html#vs-code-configuration If you are already familiar with another functional programming language, OCaml will be quick to pick up. If you're new to functional programming, however, you might want to spend some time at the beginning of the semester getting up to speed. Here are some resources for learning OCaml: * [Try OCaml][try] is a tutorial you can follow in your browser. * [The CS 3110 tutorial][3110tut] is accessible and thorough. * The book [*Real World OCaml*][rwo] is fantastic and free to read online. [rwo]: https://realworldocaml.org [3110tut]: https://www.cs.cornell.edu/courses/cs3110/2016fa/l/01-intro/rec.html [try]: https://try.ocamlpro.com (##) Textbooks You Might Like There are no required textbooks, but if you find yourself wanting extra background, you might find these textbooks helpful: * *The Formal Semantics of Programming Languages* by Glynn Winskel. * *Types and Programming Languages* by Benjamin C. Pierce. And here are a couple of good online textbooks that are relevant to the course: * [*Programming Languages: Application and Interpretation*](http://cs.brown.edu/~sk/Publications/Books/ProgLangs/) by Shriram Krishnamurthi. * [*Software Foundations*](https://www.cis.upenn.edu/~bcpierce/sf/) by Benjamin C. Pierce and a supporting cast. (##) LambdaLab Adrian Sampson made an experimental web-based tool, called [LambdaLab][], to help you learn the λ-calculus. You can type in terms to reduce them, and you can define and use encodings. It's open source and [on GitHub][llgh], and contributions are welcome. [lambdalab]: https://capra.cs.cornell.edu/lambdalab/ [llgh]: https://github.com/cucapra/lambdalab (##) Extra Background Here are some well-written materials on standard PL topics: * For a self-contained overview of *structural induction*, see [some notes by John A. Thywissen for a class at UT Austin][thywissen]. * For an overview of notation for inference rules, semantics, and types, see this [crash-course blog post by Jeremy Siek][siek]. [siek]: https://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html [thywissen]: https://www.cs.utexas.edu/%7Ejthywiss/Structural%20Induction%20in%20Programming%20Language%20Semantics.pdf (##) LaTeX There are many options for typesetting inference rules and derivation rules in LaTeX. We recommend [mathpartir][], which is included with most TeX distributions. [mathpartir]: http://cristal.inria.fr/~remy/latex/mathpartir.html # Schedule We will update this every week with planning lecture notes! Date | Topic | Readings | Assignments :------:|-------|----------|:-----------: Jan 23 | Course Overview | notes | Jan 25 | λ-calculus | notes | Jan 27 | More λ-calculus | same notes
more notes| Jan 30 | λ-calculus Encodings | notes| Out: A01 Feb 01 | Reduction Strategies | notes| Feb 03 | Operational Semantics | same notes| Feb 06 | Fixed points | notes| Feb 08 | Mutual recursion | post| Feb 10 | Well-founded induction | notes| Feb 13 | Inductive definitions and lfp | notes
extra notes| Feb 15 | Knaster-Tarski | same notes| Out: A02 Feb 17 | The IMP language | notes| Feb 19 | Small-Step semantics | same notes| Feb 21 | Big-Step Semantics and Evaluation Contexts | notes| Feb 24 | Semantics via Translation | notes| Feb 27 | Semantics via Translation (ctd) | same notes| Mar 1 | A functional language | notes
extra notes| Mar 3 | no lecture | | Mar 6 | Recursion and scoping | notes| Mar 8 | State | notes| Mar 10 | Continuations | notes| Mar 13 | Exceptions | notes| Mar 15 | Exceptions | notes| Mar 17 | no lecture | | Out: Prelim Mar 20 | Hoare Logic | notes | Mar 22 | Hoare Logic cont'd | same notes | Mar 24 | Predicate Transformers | notes | Mar 27 | Dynamic Logic and Kleene Algebra | notes | Mar 29 | Kleene Algebra with tests | same notes | Mar 31 | NetKAT | paper | Apr 10 | NetKAT ct'd | paper | Apr 12 | Typed Lambda Calculus | notes | Out: A03 Apr 14 | Products, Sums, Datatypes | notes | Apr 17 | no lecture | extra notes | Apr 19 | Strong Normalization | notes | Apr 21 | Type Inference | notes | Apr 24 | Subtyping | notes | Apr 26 | Polymorphic lambda-calculus | notes | Apr 28 | Recursive Types | notes | May 1 | Probabilistic IMP and weakest-pre expectation | notes
extra notes | Out: Exam May 3 | PL at Jane Street (Ron Minsky) | | May 5 | Propositions as Types and Curry-Howard | notes
more notes | May 8 | Wrap-up | | # Policies (##) Academic Integrity Absolute integrity is expected of all Cornell students in every academic undertaking. Cornell University has a Code of Academic Integrity (see [here](https://theuniversityfaculty.cornell.edu/dean/academic-integrity/)). Violations of this code are treated very seriously by Cornell and can have long-term repercussions. On **assignments**, everything you turn in must be 100% completely your own work (with your partner, if you have one). You may discuss with other students about requirements for the assignment, programming in OCaml, etc. But when it comes to developing specific answers or coding, you may not talk to other students except for your partner. Specifically: * Do not show any partial solution to another student or give any hints. * Never share code. (Shared code is surprisingly easy to detect.) * Do not search the Internet for solutions. Don't look anything relevant up on Wikipedia. Don't search on Stack Overflow or anywhere else. * *Do* ask someone if you're confused about what the assignment is asking for. * *Definitely* ask the course staff if you're not sure whether or not something is OK. Here's the policy for **exams**: outside of the course staff, you may not talk to anyone about any exam content at all until the exam is graded. Don't even tell anyone how you're feeling about the exam or what you found challenging: you must pretend that you have never seen the exam. You can use notes from the class, including both your own notes and our notes from the website, but not outside resources. You may not give any hints or post any code that might be part of a solution on Slack (except in a private message with course staff). On both assignments and exams, the web is always off limits: you may not Google anything or look anything up on Wikipedia to get help, for example. (##) Respect in Class Everyone---the instructor, TAs, and students---must be respectful of everyone else in this class. All communication, in class and online, will be held to a high standard for inclusiveness: it may never target individuals or groups for harassment, and it may not exclude specific groups. That includes everything from outright animosity to the subtle ways we phrase things and even our timing. For example: do not talk over other people; don't use male pronouns when you mean to refer to people of all genders; avoid explicit language that has a chance of seeming inappropriate to other people; and don't let strong emotions get in the way of calm, scientific communication. If any of the communication in this class doesn't meet these standards, please don't escalate it by responding in kind. Instead, contact the instructor as early as possible. If you don't feel comfortable discussing something directly with the instructor---for example, if the instructor is the problem---please contact the advising office or the department chair. (##) Special Needs and Wellness It is Cornell policy to provide reasonable accommodations to students who have a documented disability (e.g., physical, learning, psychiatric, vision, hearing, or systemic) that may affect their ability to participate in course activities or to meet course requirements. Students with disabilities are encouraged to contact [Student Disability Services](http://sds.cornell.edu/) at 607-254-4545, or the instructor for a confidential discussion of their individual needs. If you are experiencing undue personal or academic stress at any time during the semester or need to talk to someone who can help, contact the instructor or: - [Engineering Academic Advising](https://www.engineering.cornell.edu/resources/advising/) at 607-255-7414, - [Learning Strategies Center](http://lsc.cornell.edu/) at 607-255-6310, - [Let's Talk Drop-in Counseling](https://health.cornell.edu/services/counseling-psychiatry/lets-talk) at Gannett at 607-255-5155 - [Empathy Assistance and Referral Service](http://orgsync.rso.cornell.edu/org/ears) at 607-255-EARS.