Underground Reading Group
Programming Languages
Spring 2016 — Friday, 2:30pm — CSE 674
Subscribe to the calendar: iCal or Google Calendar.| Date | Who | What |
|---|---|---|
|
Mar 31
|
everyone |
Organizational meeting |
|
Apr 7
|
James W |
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega |
|
Apr 15
|
Doug Woos |
Learning Invariants using Decision Trees and Implication Counterexamples and please skim Decidability of Inferring Inductive Invariants |
|
Apr 22
|
Doug and James |
Ivy: Safety Verification by Interactive Generalization |
|
Apr 29
|
Talia |
F-ing Modules |
|
May 6
|
Nate |
Cubical Type Theory |
|
May 13
|
Konstantin Weitz |
The Denotational Semantics of Programming Languages |
|
May 20
|
Thomas Lou |
Morphoid Type Theory (Sections 1 and 2 only) |
|
May 27
|
Alex Sanchez-Stern |
Symbolic Abstract Data Type Inference |
|
Jun 3
|
Everyone |
Cubical Type Theory |
Paper Suggestions
- Meta-theory a la Carte
- Programming with Intersection Types and Bounded Polymorphism
- A simple type-theoretic language: Mini-TT
- Morphoid Type Theory
- COGENT: Verifying High-Assurance File System Implementations (ASPLOS’16)
- How to Build Static Checking Systems Using Orders of Magnitude Less Code (ASPLOS’16)
- Symbolic Abstract Data Type Inference (POPL’16)
- Chapar: Certified Causally Consistent Distributed Key-Value Stores (POPL’16)
- Query-Guided Maximum Satisfiability (POPL’16)
- Printing Floating-Point Numbers: A Faster, Always-Correct Method (POPL’16)
- Example-Directed Synthesis: A Type-Theoretic Interpretation (POPL’16)
Contact James W (jrw12@cs) if you want to get on the mailing list. Or subscribe yourself.