Schedule
The following schedule lists the topics we will cover and approximately the number of meetings we will spend on each topic. The schedule is tentative. Most likely, some things will change during the semester, and I will revise the schedule as necessary.
The Reading column lists the assigned reading for the meeting. You should view the readings as an introduction to spark discussion in class.
The Assignment column lists the due date for each assignment.
The readings will be classified into the following order of recommendation:
- Advised (i.e., expected, required, and of highest importance) — assigned.
- Recommended (i.e., important but read after previous category) — assigned.
- Supplemental (i.e., additional material for a different perspective) – optional.
- Fun (i.e., related fun additional material) – optional.
Week-By-Week
| Week | Date | Topic | Reading | Assignment | |
|---|---|---|---|---|---|
| 1 | T | 8/29 | Welcome and course overview meeting01 |
Post a note on Piazza to introduce yourself. Review the Course Syllabus. | |
| R | 8/31 | Classic application: Model checking and counterexample-guided abstraction refinement meeting02 meeting02-hw00 meeting02-slides |
Supplemental. Thomas Ball and Sriram K. Rajamani. The SLAM Project: Debugging System Software via Static Analysis. Symposium on Principles of Programming Languages (POPL), 2002. Supplemental. Thomas Ball and Sriram K. Rajamani. Automatically Validating Temporal Safety Properties of Interfaces. International SPIN Workshop, 2001. Recommended. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Lazy Abstraction. Symposium on Principles of Programming Languages (POPL), 2002. Software model checking with counterexample-guided abstraction refinement marked a major milestone in taking automated reasoning techniques into industrial practice. |
||
| 2 | T | 9/5 | Judgments and rules | Advised. Harper Ch. 1.1; Winskel Ch. 1 and 3.1-3.3. Provides some preliminaries for HW0 (optional depending on your background). Rest of Harper Ch. 1 is helpful but “supplemental” for HW0. Supplemental. Pierce Ch. 2 and 3.1-3.3. Another take on mathematical preliminaries for HW0 (optional depending on your background). |
|
| R | 9/7 | Judgments and rules | Advised. Harper Ch. 2. It is ok to skim 2.4 and 2.6-2.7 for now. |
HW0 due Fri | |
| 3 | T | 9/12 | Statics and dynamics | Advised. Harper Ch. 3 It is ok to skim 3.3-3.4 for now. Advised. Winskel Ch. 2 Sections 2.1-2.5 defines a big-step operational semantics for a simple imperative language IMP. Then, Section 2.6 sketches a small-step operational semantics. |
|
| R | 9/14 | Statics and dynamics | Advised. Harper Ch. 4-5 and 7.1-7.2 It is ok to skim 5.4 for now. Recommended. Pierce 3.4 A high-level overview of the three basic approaches to formalizing semantics. |
||
| 4 | T | 9/19 | Type safety | Advised. Harper Ch. 6 and 7.3 About type safety. Supplemental. Pierce 3.5 and Ch. 8 Another take on operational semantics and type safety. |
|
| R | 9/21 | Type safety | Advised. Harper 2.4; Winskel 3.4 and Ch. 4 Revisit induction on derivations. |
HW1 due Fri | |
| 5 | T | 9/26 | Functions | Advised. Harper 8.1-8.2, 9.1-9.2, and 10.1-10.2 (Functions). Sections 8.3-8.4, 9.3-9.4, and 10.3 can be considered supplemental. |
|
| R | 9/28 | Finite data types | Advised. Harper Ch. 11.1-11.2 and 12.1-12.3 (Products and Sums). It is ok to skim 11.2 and 12.2-12.3. Section 11.3 can be considered supplemental. |
||
| 6 | T | 10/3 | Imperative computation | Recommended. Review Winskel Ch. 2 Supplemental. Harper Ch. 34-35 |
|
| R | 10/5 | Imperative computation | HW2 due Fri | ||
| 7 | T | 10/10 | Recursion | ||
| R | 10/12 | Recursion | |||
| 8 | T | 10/17 | Denotational semantics | Advised. Winskel Ch. 5 | |
| R | 10/19 | Denotational semantics | Advised. Winskel Ch. 8 Read for the general concepts, not the details. Supplemental. David Schmidt. Denotational Semantics: A Methodology for Language Development. This is a full textbook on denotational semantics. |
||
| 9 | T | 10/24 | Recursive types | Advised. Harper 16.1-16.2 and 15.1 (Recursion and Recursive Types). Sections 16.3-16.5 and 15.2-15.4 can be considered supplemental. |
|
| R | 10/26 | Parametric polymorphism | Advised. Harper 20.1 (Parametric Polymorphism). Sections 20.2-20.3 can be considered supplemental. Recommended. Harper 21.1 (Abstract Types) Sections 21.2-21.4 can be considered supplemental. |
||
| 10 | T | 10/31 | Denotational semantics | ||
| R | 11/2 | Recursive types | HW3 due Fri | ||
| 11 | T | 11/7 | Axiomatic semantics | Advised. Winskel Ch. 6 Recommended. Winskel Ch. 7. It is ok to skim 7.1 and 7.3. |
|
| R | 11/9 | Abstract machines | Advised. Harper 27.1-27.2 (Control Stacks). Sections 27.3 can be considered supplemental. Recommended. Harper 28.1-28.2 and 29.1-29.2 (Exceptions and Continuations). Sections 28.3-28.4 and 29.3 can be considered supplemental. |
||
| 12 | T | 11/14 | Verification-condition generation | ||
| R | 11/16 | Abstract interpretation | HW4 due Fri | ||
| 13 | T | 11/21 | No class: Thanksgiving | ||
| R | 11/23 | No class: Thanksgiving | |||
| 14 | T | 11/28 | Research application | ||
| R | 11/30 | Final exam preparation | |||
| 15 | T | 12/5 | Related work presentations | ||
| R | 12/7 | Related work presentations | |||
| 16 | T | 12/12 | Final project presentations | ||
| R | 12/14 | Final project presentations | |||
| 17 | T | 12/19 | No class: Finals week | Paper due Sun |
Final Project Presentations
Tue 12/12
- 2:00pm-2:35pm: Abhishek Purshothama and Christian Fontenot: Goal-Directed Abstract Interpretation of Distributed Systems with Pâtissier
- 2:35pm-3:10pm: David Baines and Matt Buchholz: Improving convergence time in PL-focused LLMs in limited training data environments via optimized syntactical learning task selection
Thu 12/14
- 2:00pm-2:35pm: Scott McCall and Zilong Li: Developing Programming Languages for Ease of Use with LLM’s
- 2:35pm-3:10pm: Karthik Sairam, Lawerence Khadka, and Emily Parker: Static Analysis of React Hooks
Abhishek Purshothama and Christian Fontenot: Goal-Directed Abstract Interpretation of Distributed Systems with Pâtissier
Reasoning about the correctness of parameterized systems such as distributed systems is challenging because an analysis framework needs to reason about an unspecified number of components. However, these systems exhibit a significant amount of regularity in both structure and communication which can be identified and leveraged to simplify the reasoning. We present a goal-directed abstract interpretation approach for the verification of distributed systems. This approach is implemented in Pâtissier, a framework for reasoning about safety properties of programs written in the P language.
David Baines and Matt Buchholz: Improving convergence time in PL-focused LLMs in limited training data environments via optimized syntactical learning task selection
Large language models (LLMs) have gained popularity in recent years for aiding programmers in coding tasks, such as code generation and summarization. However, as new programming languages are continually introduced and adopted, existing code LLMs may not generalize well to unseen languages; further, existing code LLM training techniques, which typically rely on large amounts of data, may not be well-suited to an emerging, low-resource programming language. In this paper, we draw inspiration from models for low-resource natural languages (NLs); we explore how syntax-driven pre-training tasks can augment the performance of a code LLM on downstream tasks, and how the relative effectiveness of modified pre-training changes with the amount of data available. We demonstrate how these augmented training techniques can help bootstrap a code LLM for an emerging programming language, with the goal of reducing the barrier to developing tools for a new programming language (e.g. an autocomplete model for programming in said language).
Scott McCall and Zilong Li: Developing Programming Languages for Ease of Use with LLM’s
In this paper, we discuss the importance of prompting in large language models, and how performance on certain tasks greatly varies based on the quality and manner of the prompt itself, which can make interacting with these models difficult. Addressing these limitations is important due to the increased mainstream usage of large language models such as ChatGPT in a wide variety of contexts. The difficulty from improving the performance of these models comes from the billions of parameters that are used in these models, and the idea that fine-tuning them would be impractical for most users and impossible for models that are closed-source. Prompting is a good approach to retrieve satisfactory responses from large languages models, and it is user-friendly since using the natural language is enough. However, many prompting methods are associated with certain templates and the call of languages models’ APIs. Our goal is to develop a programming language that can interact with an LLM such as ChatGPT in a way such that constraints and other conditions can be added to the prompt such that it provides a layer of abstraction to the user that makes it easier to interact with the LLM in a way that provides higher quality results.
Karthik Sairam, Lawerence Khadka, and Emily Parker: Static Analysis of React Hooks
Hooks provide an ergonomic model for reasoning about states and effects in React.js components. But, they come with their own set of rules that the developers must manually abide by. Without a strict compile time verification of those rules, there exist chances of subtle bugs, slower than expected performance issues and infinite re-rendering of the UI, which can occur completely unbeknownst to the developer until the app is actually run. In this paper, we try to model the behaviour of these hooks in terms of the React Concurrent Fiber Architecture to identify such bugs much earlier in the development cycle.
Post Introduction and Background
Post a note on Piazza to introduce yourself and tell me about your background.
What’s your background?
- Comfort with functional programming?
- Comfort with mathematical logic and induction?
- Experience with building language tools (interpreters, translators)?
- What do you want out of this class?
If you prefer, you can send a separate private note to me about your background.