University of Chicago Programming Languages Reading Group University of Chicago Programming Languages Reading GroupThe Programming Languages Reading Group, part of PL research at UChicago, is an occasional, informal meeting to discuss interesting PL papers. Food is provided. Visitors welcome!
To receive announcements, sign up for the pl-readinggroup mailing list.
To suggest a paper, open an issue on the Github page. We’ll close the issue when we schedule the paper.
For Spring 2023, PLRG meets on Tuesdays 12pm in Crerar 354.
| Date | Paper | Leader |
|---|
| Date | Paper | Leader |
|---|---|---|
| January 20 | Comonads are Objects | Nathan |
| January 27 | Strong Normalization from Weak Normalization in Typed Lambda-Calculi | Nathan |
| February 3 | DimSum: A Decentralized Approach to Multi-language Semantics and Verification | Bhakti |
| February 10 | Introduction to Free Monads | Matt |
| February 17 | Polymorphism, subtyping, and type inference in MLsub | John |
| February 24 | The simple essence of algebraic subtyping: principal type inference with subtyping made easy | John |
| March 3 | Reflection without Remorse & Asymptotic Improvement of Computations over Free Monads | Skye |
| Date | Paper | Leader |
|---|---|---|
| October 18 | Staged Compilation with Two-Level Type Theory (POPL '22) & staged-fusion | Skye |
| October 25 | (Staged Compilation continued) | Skye |
| November 1 | Type-Preserving CPS Translation of Sigma and Pi Types is Not Not Possible (POPL '18) | Nathan |
| November 8 | Incorrectness Logic (POPL '20) | Bhakti |
| November 15 | Free Monads and Algebraic Effects | Skye |
| November 22 | Algebraic Effects and Koka | Byron |
| November 28 | Genetic Programming with Polymorphic Types and Higher-Order Functions | Andy |
For the Spring 2020 term, PLRG meets on Wednesdays, 3:00pm at https://uchicago.zoom.us/j/564109413.
Reading group did not meet for the Fall 2019 term and Winter 2020 terms because everybody was distracted.
For the Spring 2019 term, PLRG met on Tuesdays, 3:00pm in Crerar 236.
Reading group did not meet for the Fall 2018 term, because of Stu’s “The Little Typer” Seminar, John’s Coq Seminar, and paper deadlines. Winter 2018 was also skipped because nobody was thinking about PLRG.
For the Summer 2018 term, we met on Fridays at various times and places.
| Date | Paper | Leader |
|---|---|---|
| 2018–6–29 | Towards a Strongly Typed Functional Operating System (IFP '02) | Brian |
| 2018–7–6 | Lunch to welcome Nick | Ravi |
| 2018–7–13 | A discussion of atJIT (Related Paper #1, Paper #2) | Kavon |
| 2018–7–20 | — | — |
| 2018–7–27 | NLP/ML + PL | Brian |
| 2018–8–3 | Fungi: Typed Incremental Computation With Names (Preprint) | Nick |
| 2018–8–10 | Bidirectional Evaluation with Direct Manipulation (OOPSLA '18) | Mikaël |
| 2018–8–17 | — | — |
| 2018–8–24 | — | — |
| 2018–8–31 | — | — |
| 2018–9–7 | — | — |
| 2018–9–14 | Output-Directed SVG Programming (draft) | Brian |
| 2018–9–21 | Practice Talk Party (ICFP, Elm Conf, Strange Loop, FHPC) | Cyrus, Ravi, Kavon |
For the Spring 2018 term, we met on Tuesdays, 12:30pm-1:30pm in Eckhart 129.
| Date | Paper | Leader |
|---|---|---|
| 2018–4–10 | OOPSLA Draft | Cyrus |
| 2018–4–17 | Contification using Dominators (ICFP '01) | Kavon |
| 2018–4–24 | Challenges in Higher-Order Superoptimization (presentation on possible thesis topic) | Kavon |
| 2018–5–1 | Weird Machines, Exploitability, and Provable Unexploitability (IEEE TETC '17) | Joe |
| 2018–5–8 | Tangible Functional Programming (IFCP '07) (Google TechTalk Video) | Brian |
| 2018–5–15 | Molecular Programming Overview; 1. JoCaml Tutorial 2. The Reflexive CHAM and the Join Calculus (POPL '96) | Joe |
| 2018–5–22 | Deuce: A Lightweight User Interface for Structured Editing (ICSE '18 Practice Talk) (Demo Video) (Silent Demo of User Study Tasks) | Brian |
For the Winter 2018 term, we met on Tuesdays, 2pm-3pm in Eckhart 129.
| Date | Paper | Leader |
|---|---|---|
| 2018–1–9 | A Principled Approach to Ornamentation in ML (POPL '18) | Joe |
| 2018–1–16 | Hazelnut: A Bidirectionally Typed Structure Editor Calculus (POPL '17) (Demo) | Cyrus |
| 2018–1–23 | Postponed by Illness | — |
| 2018–1–30 | 1ML – Core and Modules United (JFP '16) | Brian |
| 2018–2–6 | Every Bit Counts: The Binary Representation of Typed Data and Programs (JFP '12) | Joe |
| 2018–2–13 | The Next 700 Programming Languages (CACM '66) & Why Concatenative Programming Matters (Blog post '12) | Kartik & Joe |
| 2018–2–20 | Sketch-n-Sketch WIP Demo | Brian |
| 2018–2–27 | ICFP Drafts | Joe & Kavon |
| 2018–3–6 | ICFP Draft | Cyrus |
For the Fall 2017 term, we met on Thursdays, 3pm-4pm in Ryerson 276.
| Date | Paper | Leader |
|---|---|---|
| 2017–11–09 | Structured Asynchrony with Algebraic Effects (TyDe '17) (Video) | Brian |
| 2017–11–16 | Tracing Lazy Functional Computations Using Redex Trails (PLILP '97) | Brian |
| 2017–11–23 | Thanksgiving | — |
| 2017–11–30 | Type Directed Compilation of Row-Typed Algebraic Effects (POPL '17) | Kavon |
| 2017–12–07 | — | — |
| 2017–12–14 | Functional Programs That Explain Their Work (ICFP '12) (Video) | Brian |
Reading Group did not meet during the Spring 2017 term. The Program Synthesis Seminar crowded it out.
For the Winter 2017 term, we met on Fridays, 11:30–12:30pm in Ryerson 277.
| Date | Paper | Leader |
|---|---|---|
| 2017–1–13 | Polymorphism, Subtyping, and Type Inference in MLsub (POPL '17) (ICFP '15 Video) | Brian |
| 2017–1–20 | Compiling Without Continuations (In submission) | Kavon |
| 2017–1–27 | Learning Refinement Types (ICFP '15) (Video) | Brian |
| 2017–2–03 | Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT) (draft) | Brian |
| 2017–2–10 | — | — |
| 2017–2–17 | Language primitives and type discipline for structured communication-based programming (ESOP '98) | Brian |
| 2017–2–24 | Programming with Algebraic Effects and Handlers | Joe |
| 2017–3–03 | — | — |
| 2017–3–10 | — | — |
| 2017–3–17 | Retrofitting Linear Types (In submission) | Joe |
For the Fall 2016 term, we met on Fridays, 12:30pm-1:30pm in Ryerson 276.
| Date | Paper | Leader |
|---|---|---|
| 2016–10–14 | Semi-Automated SVG Programming via Direct Manipulation | Brian |
| 2016–10–21 | Automatic Generation of Peephole Superoptimizers | Kavon |
| 2016–10–28 | Dag-Calculus: A Calculus for Parallel Computation | Kavon |
| 2016–11–04 | A correspondence between rooted planar maps and normal planar lambda terms | Joe |