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)

Verified compilation

Week 7 (presentations on Mon 24 November 2025)

Partial evaluation

Week 8 (presentations on Mon 1 December 2025)

Program synthesis