PL Reading Group @ IU
Spring 2022 馃尫
About
The PL Reading Group (PLRG) is the de facto successor to PL Wonks and several previous reading groups. Unlike PL Wonks talk series, the focus of PLRG is paper reading and discussion. However, we do occasionally schedule presentations, practice talks, and tutorial sessions (Schedule).
We are looking for presentations! Please visit the "participating" page for details about voting for papers to read and scheduling your presentation.
Time
- Time: <4:00 PM> on Tuesdays.
- The event usually lasts 1 hour. You may leave early.
- If you are a speaker, please make sure your presentation is within 40 minutes.
Location
- Room: BLIF-4105 (study room, 4th floor Luddy Hall)
- Where is it? Search "Luddy Hall" on Campus Map.
Schedule
Date | Paper Title / Presentation | Speaker(s) |
---|---|---|
POPL Week | N/A | |
Paper Reading: | Group Discussion | |
A Correspondence between Continuation Passing Style | ||
and Static Single Assignment Form | ||
Links: 1 , ACM-DL , Scheme->CPS Code | ||
Presentation: Recursive Types | Kartik | |
Links: LaTeX for Slides , Racket Code , Haskell Code | ||
Paper Reading: Compilers and Staging Transformations | Group Discussion | |
Links: 1 , ACM-DL | ||
Presentation: | Chenchao | |
位-circuit: Reasoning About 位-calculus Diagrammatically | ||
Links: Slides | ||
Presentation: | Hazel | |
Categories, parametricity, and a folk theorem | ||
Links: Agda Formalization, Further Reading 1, | ||
Further Reading 2, Racket for Slides | ||
Paper Reading: Domains for Denotational Semantics | Group Discussion | |
Links: 1 , ACM-DL | ||
Paper Reading: | Group Discussion | |
A theory of type polymorphism in programming | ||
Links: 1 , DOI | ||
Spring Break | N/A | |
Paper Reading: Data Types as Lattices | Group Discussion | |
Links: 1 , DOI | ||
Paper Reading: The mechanical evaluation of expressions | Group Discussion | |
Links: 1 , DOI | ||
Paper Reading: Call-by-name, call-by-value, and | Group Discussion | |
the 位-calculus Links: 1 , DOI | ||
Paper Reading: A structural approach to operational | Group Discussion | |
semantics Chapters 1~3 Links: 1 , 2 | ||
Paper Reading: Control Operators, the SECD-Machine, | Group Discussion | |
and the 位-Calculus Links: 1 | ||
Paper Reading: Natural semantics | Group Discussion | |
Links: 1 | ||
Paper Reading: A Functional Correspondence between | Group Discussion | |
Evaluators and Abstract Machines | ||
Links: 1 | ||
Presentation: Semantic Subtyping | Kartik | |
Links: Reference on Semantic Subtyping | ||
Presentation: ACL2 and J-Bob | Kartik | |
References: Computer-Aided Reasoning: An Approach by | ||
Kaufman, Manolios and Moore; The Little Prover by Friedman | ||
and Eastlund | ||
Paper Reading: Type-Preserving Renaming and | Group Discussion | |
Substitution | ||
Links: 1 | ||
Paper Reading: A Syntactic Approach to Type Soundness | Group Discussion | |
Links: 1 | ||
Paper Reading: Fast and Effective Procedure Inlining | Group Discussion | |
Links: 1 | ||
Paper Reading: Call-by-Push-Value: A Subsuming Paradigm | Group Discussion | |
Links: 1 | ||
Paper Reading: The Derivative of a Regular Type is its Type of One-Hole Contexts | Group Discussion | |
Links: 1 | ||
Paper Reading: An Axiomatic Basis for Computer Programming | Group Discussion | |
Links: 1 | ||
Paper Reading: Functional Pearls: Probabilistic Functional Programming in Haskell | Group Discussion | |
Links: 1 | ||
Presentation: Automating Proofs by Induction | Kartik | |
Links: Implementation Notes | ||
Paper Reading: Full Abstraction for PCF | Group Discussion | |
Links: Paper, Previous Paper on Game Semantics, Notes from OPLSS | ||
Presentation Classical Realizability | Darshal | |
Links: Reference |