Advanced topics in programming languages

Tentative seminar schedule

Seminars take place at 11am on Mondays in FW26, except for the first week, which will take place at 11am on Friday in the same room.

Week 1 (Fri 10 October 2025)

Introduction
Materials:

• Introduction slides
  

Week 2 (presentations on Mon 20 October 2025)

Taming functions
Materials:

• Taming functions slides
  

Assigned papers:

• Defunctionalization at Work
  (PPDP 2001)
  Olivier Danvy and Lasse R. Nielsen
• Typed closure conversion
  (POPL 1996)
  Yasuhiko Minamide, Greg Morrisett and Robert Harper
• Lambda-Lifting in Quadratic Time
  (FLOPS 2002)
  Olivier Danvy and Ulrik P. Schultz

Week 3 (presentations on Mon 27 October 2025)

Effect handlers
Materials:

• Effect handler slides (and accompanying example)
  

Background reading (optional):

• An Introduction to Algebraic Effects and Handlers (Matija Pretnar, 2015)
• Foundations for Programming and Implementing Effect Handlers (Daniel Hillerström, 2021)

Assigned papers:

• Retrofitting effect handlers onto OCaml
  (PLDI 2021)
  KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, Anil Madhavapeddy
• Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C
  (ICFP 2021)
  Ningning Xie, Daan Leijen
• Do Be Do Be Do
  (POPL 2017)
  Sam Lindley, Conor McBride, Craig McLaughlin

Week 4 (presentations on Mon 3 November 2025)

Dependent types
Materials:

• Dependent types slides
  

Assigned papers:

• The Size-Change Principle for Program Termination
  (POPL 2001)
  Chin Soon Lee, Neil D. Jones and Amir M. Ben-Amram
• IDRIS ---: systems programming meets full dependent types
  (PLPV 2011)
  Edwin C. Brady
• Why Dependent Types Matter
  (Unpublished, 2005)
  Thorsten Alternkirch, Conor McBride and James McKinna

Week 5 (presentations on Mon 10 November 2025)

Module systems

• Module systems slides
  

Background reading (optional):

• Section 11 (Related work and discussion) of F-ing modules, extended version (Andreas Rossberg, Claudio Russo and Derek Dreyer, JFP 2014)
• Chapter 1 (The Design Space of ML Modules) of Understanding and Evolving the ML Module System (Derek Dreyer, 2005)

Assigned papers:

• A Type-Theoretic Approach to Higher-Order Modules with Sharing
  (POPL 1994)
  Robert Harper and Mark Lillibridge
• Applicative Functors and Fully Transparent Higher-Order Modules
  (POPL 1995)
  Xavier Leroy
• F-ing Modules
  (TLDI 2010)
  Andreas Rossberg, Claudio Russo, and Derek Dreyer

Week 6 (presentations on Mon 17 November 2025)

Partial evaluation
Materials:

• Partial evaluation slides
  

Background reading (optional):

• Partial Evaluation and Automatic Program Generation (N.D. Jones, C.K. Gomard, and P. Sestoft, 1993)

Assigned papers:

• Continuation-based partial evaluation
  (LISP and Functional Programming, 1994)
  Julia L. Lawall and Olivier Danvy
• Eta-Expansion Does The Trick
  (TOPLAS, 1996)
  Olivier Danvy, Karoline Malmkjær, and Jens Palsberg
• The essence of LR parsing
  (PEPM, 1995)
  Michael Sperber and Peter Thiemann

Week 7 (presentations on Mon 24 November 2025)

Verified compilation
Materials:

• Verified compilation slides
  

Assigned papers:

• A formally verified compiler back-end
  (Journal of Automated Reasoning, 2009)
  Xavier Leroy
• CakeML: A Verified Implementation of ML
  (POPL, 2014)
  Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens
• Certified code generation from CPS to C
  (2018)
  Olivier Savary Bélanger, Matthew Z. Weaver, and Andrew W. Appel

Week 8 (presentations on Mon 1 December 2025)

Program synthesis
Materials:

• Program synthesis slides
  

Background reading (optional):

• Program Synthesis (S. Gulwani, O. Polozov and R. Singh, 2017.)

Assigned papers:

• Type-and-example-directed program synthesis
  (PLDI 2015)
  Peter-Michael Osera and Steve Zdancewic
• Program Synthesis from Polymorphic Refinement Types
  (PLDI 2016)
  Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama
• Recursive Program Synthesis using Paramorphisms
  (PLDI 2024)
  Qiantan Hong and Alex Aiken