Software systems around us are getting more and more complex by the day with multi-processor systems, microservices, and distributed programming. At the center of all this complexity lies concurrency, i.e., processes can execute in arbitrary orders and failures (e.g., network faults, node crashes, etc.) are pervasive. Building software systems is no longer straightforward (probably never was) and the issues introduced by concurrency cannot be ignored. This course will study the foundations of where these challenges arise from and will equip students with tools to handle these challenges.
The ultimate goal is for students to build robust concurrent software systems using state-of-the-art PL tools and techniques.
| Instructor: | Ankush Das, ankushd [at] bu [dot] edu |
| Class Schedule: | Mon & Wed, 4:30pm - 5:45pm |
| Class Location: | MCS B29 |
| Office Hours: | Wed, 9am - 10am, CDS 721 (or with appointment with instructor) |
| Piazza: | Please join the class using the following link: https://piazza.com/bu/spring2024/cs599d1. We will be using Piazza for class announcements and discussions. |
| Gradescope: | Please sign up for a student account on https://gradescope.com using your BU email address. The entry code for the course is XX438J. Homework assignments are to be submitted to Gradescope in PDF format. |
| Course Website: | https://ankushdas.github.io/CS599.html |
Will be updated regularly!
| Date | Topics | Lecture Notes | Further Reading |
|---|---|---|---|
| Jan 22, 2024 | LL1: A Language for Arithmetic Expressions | Lecture 1 | |
| Jan 24, 2024 | Untyped Lambda Calculus | Lecture 2 | |
| Jan 29, 2024 | An Introduction to Types | Lecture 3 | |
| Jan 31, 2024 | Simply-Typed Lambda Calculus | Lecture 4 | |
| Feb 5, 2024 | Substructural Inference and Logic | TBA | Notes by Frank Pfenning |
| Feb 7, 2024 | Linear and Ordered Inference | TBA | Notes by Frank Pfenning |
| Feb 12, 2024 | Harmony: Identity and Cut Admissibility | TBA | Notes by Frank Pfenning |
| Feb 19, 2024 | President's Day: No Lecture | ||
| Feb 21, 2024 | Session Typed Proof Terms | TBA | Chapter 2.1 from PhD Thesis |
| Feb 26, 2024 | Session Typed Proof Terms (Continued) | TBA | Chapter 2.1 from PhD Thesis |
| Mar 4, 2024 | Mid-Term | NA | |
| Mar 6, 2024 | Mid-Term Discussion | TBA | Chapter 2.1 from PhD Thesis |
| Mar 11, 2024 | Spring Break | ||
| Mar 13, 2024 | Spring Break | ||
| Mar 18, 2024 | Semantics of Session Types | TBA | Chapter 2.1 from PhD Thesis |
| Mar 20, 2024 | Session Type Configurations | TBA | Chapter 2.1 from PhD Thesis |
| Mar 25, 2024 | Preservation Theorem | TBA | Chapter 2.1 from PhD Thesis |
| Mar 27, 2024 | Progress Theorem | TBA | Chapter 2.1 from PhD Thesis |
| Apr 1, 2024 | Co-Induction and Session Type Equality | TBA | Subtyping for Session Types |
| Apr 3, 2024 | Refinement Session Types I | TBA | Chapter 3 from PhD Thesis |
| Apr 8, 2024 | Refinement Session Types II | TBA | Chapter 3 from PhD Thesis |
| Apr 15, 2024 | No Lecture | ||
| Apr 17, 2024 | Refinement Types: Examples | TBA | Chapter 3 from PhD Thesis |
| Apr 22, 2024 | Shared Session Types | TBA | Balzer et. al., ICFP 2017 |
| Release Date | Due Date | Assignment PDF | Template TEX |
|---|---|---|---|
| Jan 22, 2024 | Feb 7, 2024 | Assignment 1 | (Template 1) |
| Feb 7, 2024 | Feb 21, 2024 | Assignment 2 | (Template 2) |
| Feb 27, 2024 | NA | Mock Mid-Term | Mock Mid-Term Solution |
| Mar 4, 2024 | NA | Mid-Term Solution | |
| Mar 5, 2024 | Mar 20, 2024 | Assignment 3 | (Template 3) |
| Mar 20, 2024 | Apr 5, 2024 | Assignment 4 | (Template 4, Code 4) |
| Apr 5, 2024 | Apr 22, 2024 | Assignment 5 | |
| Apr 22, 2024 | May 1, 2024 | Assignment 6 |
The course grade will be calculated using homework assignments, a mid-term exam, and a final exam.
There will be bi-weekly homework assignments due every other Wednesday at 11:59pm. Homeworks can sometimes be challenging, so it is best to start early to give yourself enough time to think attempt the problems and make best use of office hours. Late homework can only be accepted in extraordinary circumstances and require approval from instructor.
You are encouraged to collaborate with other students on solving the homework problems. But you must write your solutions independently in your own words (or code).
I would strongly encourage students to typeset homework solutions using LaTeX which is the most popular document preparation system used in computer science publications. But students can use different software such as MS Word or handwrite solutions. For your convenience, I will provide the LaTeX source for each assignment with instructions on how to typeset the solutions.
Exams will be held in-person and you may bring handwritten (or printed) notes to the exam. However, using other means such as internet, ChatGPT, phones, laptops, etc. is strictly prohibited.
Programming Language: Could you clarify which programming language(s) will be used in the course?
There is no fixed programming language for this course. The intent of the course is to study the foundations of a programming language in terms of the abstractions it provides (functions, variables, loops, types, etc.). These are common to most languages. That being said, there will be some programming assignments where students would be free to choose their own programming language to complete them. A small note here is that some programming assignments will be slightly easier in languages like OCaml or Rust (easier to define recursive types) but that doesn't mean that the assignments cannot be implemented in other languages.
Course Content: Is there a detailed syllabus available, e.g., topics covered, assignments, and major projects.
The course is new and the syllabus is a bit flexible and I would collect feedback from students and adjust the topics based on that. However, here are some high-level topics:
Teaching Style: Could you briefly describe your teaching style and whether the course emphasizes theory, practical implementation, or a combination of both?
The course will certainly be emphasizing theory but implementation will also be a major component. For each topic covered, we will first study the theory behind it and then implement them in your language of choice.
Coursework: What types of programming assignments can students expect? Are they related to concurrency problems or parallel program development?
No, the programming assignments will be more about concurrency than parallelism. This course will be highlighting the challenges that concurrency introduces instead of the benefits that parallel programming provides. The latter is an important point and will be covered in a lecture but not be the central focus.
Readings: Are there any recommended readings or materials that can provide deeper insights into this?
As far as reading material goes, I am working on lecture notes that will be the most relevant. As I introduce various topics, I will post some optional reading material but the lecture notes will be the most relevant.
All Boston University students are expected to maintain the highest standards of academic integrity. You can find important resources here:
Students with documented disabilities, including learning disabilities, may be entitled to accommodations intended to ensure that they have integrated and equal access to the academic, social, cultural, and recreational programs the university offers. Accommodations may include, but are not limited to, additional time on tests, staggered homework assignments, note-taking assistance. If you believe you should receive accommodations, please contact the Office of Disability Services to discuss your situation. This office can give you a letter that you can share with instructors of your classes outlining the accommodations you should receive. The letter will not contain any information about the reason for the accommodations.
Disability & Access Services
25 Buick Street, Suite 300
617-353-3658
access@bu.edu
http://www.bu.edu/disability/