Programming Languages

Paper Reading Group

Welcome to the web page of the Paper Reading Group organized by the PS working group.

Place: Room B217/218

Time: every Wednesday, 14:00-15:00, unless announced otherwise.

Organizer: Philipp Schuster.

How does our PRG work?

We read and discuss one paper per meeting. One participant (the discussion leader) will give a short summary and raise a few points for discussion, but every participant is expected to read the paper beforehand.

Guests are always welcome!

To be notified about upcoming meetings, please subscribe to our mailing list via this web interface. The schedule below for discussion leaders is tentative, beyond the next week.
For topics of high significance and technical depth, we might devote two meetings.
The role of discussion leader rotates among participants.

Feel free to propose candidates for future meetings by contacting Philipp. Modifying this webpage directly will not work reliably, as its content is auto-generated.

The PRG is also open to motivated students—see the LSF description.

Next meetings

March 20, 2019

Extensible Denotational Language Specifications

Robert Cartwright and Matthias Felleisen. Proceedings of the International Conference on Theoretical Aspects of Computer Software: 244—272 (1994)

Paper (PDF)

March 27, 2019

To determine

April 3, 2019

To determine

April 10, 2019

To determine

April 17, 2019

To determine

April 24, 2019

To determine

May 1, 2019

To determine

Previous meetings

March 13, 2019

Making Money Using Math

Erik Meijer. Queue 15(1) (2017)

Paper (PDF)

March 6, 2019

Proofs for Free: Parametricity for Dependent Types

Jean-philippe Bernardy, Patrik Jansson and Ross Paterson. J. Funct. Program. 22(2) (2012)

We will discuss sections 5, 6 and 7.

Paper (PDF)

February 6, 2019

Proofs for Free: Parametricity for Dependent Types

Jean-philippe Bernardy, Patrik Jansson and Ross Paterson. J. Funct. Program. 22(2) (2012)

We will only discuss sections 1, 2 and 3.

Paper (PDF)

January 30, 2019

On Self-Interpterters for System T and other typed λ-Calculi

Andrej Bauer (2016)

Paper (PDF)

January 23, 2019

A Walk in the Semantic Park

Olivier Danvy, Jacob Johannsen and Ian Zerny. Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation: 1—12 (2011)

Paper (PDF)

December 12, 2018

Handling Delimited Continuations with Dependent Types

Youyou Cong and Kenichi Asai. Proc. ACM Program. Lang. 2(ICFP) (2018)

We'll only discuss sections 1-4 and 6.

Paper (PDF)

November 28, 2018

Strict and Lazy Semantics for Effects: Layering Monads and Comonads

Andrew K. Hirsch and Ross Tate. Proc. ACM Program. Lang. 2(ICFP) (2018)

Paper (PDF)

November 21, 2018

Generic Programming of All Kinds

Alejandro Serrano and Victor Cacciari Miraldo. Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell: 41—54 (2018)

Paper (PDF)

October 31, 2018

Levity Polymorphism

Richard A. Eisenberg and Simon Peyton Jones. Proc. of PLDI: 525—539 (2017)

Paper (PDF)

October 24, 2018

Programming Language Foundations in Agda

Philip Wadler. Proc. of SMBF (2018)

Paper (PDF)

October 11, 2018

How Are Programs Found? Speculating About Language Ergonomics with Curry-Howard

Johannes Emerich. Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software: 212—223 (2016)

Paper (PDF)

October 4, 2018

Compiling with Continuations, Continued

Andrew Kennedy. Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming: 177—190 (2007)

Paper (PDF)

September 13, 2018

A Syntactic Approach to Type Soundness

A.K. Wright and M. Felleisen. Inf. Comput. 115(1): 38—94 (1994)

Paper (PDF)

August 23, 2018

Everybody's Got To Be Somewhere

Conor McBride. Electronic Proceedings in Theoretical Computer Science: 53—69 (2018)

Paper (PDF)

July 19, 2018

Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)

Anton Setzer and Peter Hancock. Dependently Typed Programming (2005)

Paper (PDF)

June 14, 2018

Passing a Language Through the Eye of a Needle

Roberto Ierusalimschy, Luiz Henrique De Figueiredo and Waldemar Celes. Commun. ACM 54(7): 38—43 (2011)

Paper (PDF)

May 3, 2018

On the expressive power of programming languages

Matthias Felleisen. Science of Computer Programming 17(1) (1991)

Paper (PDF)

April 5, 2018

Just Do It: Simple Monadic Equational Reasoning

Jeremy Gibbons and Ralf Hinze. Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming: 2—14 (2011)

Paper (PDF)

March 22, 2018

Separation Logic: A Logic for Shared Mutable Data Structures

John C. Reynolds. Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science: 55—74 (2002)

We will only discuss sections 1 - 7.

Paper (PDF)

March 8, 2018

First-Class Type Classes

Matthieu Sozeau and Nicolas Oury. Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics: 278—293 (2008)

Paper (PDF)

March 1, 2018

In Search of Types

Stephen Kell. Proc. of Onward!: 227—241 (2014)

Paper (PDF)

January 25, 2018

On the unity of duality

Noam Zeilberger. Annals of Pure and Applied Logic 153(1) (2008)

The focus will be on sections 2 and 3. We will not discuss the proofs in detail.

Paper (PDF)

January 11, 2018

A Monadic Framework for Delimited Continuations

R. Kent Dyvbig, Simon Peyton Jones and Amr Sabry. J. Funct. Program. 17(6): 687—730 (2007)

We will not read section 5 and only gloss over sections 6 and 7.

Paper (PDF)

December 7, 2017

An evaluation semantics for classical proofs

C. R. Murthy. Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science: 96—107 (1991)

Paper (PDF)

November 30, 2017

Unifying Structured Recursion Schemes

Ralf Hinze, Nicolas Wu and Jeremy Gibbons. Proc. of ICFP: 209—220 (2013)

Paper (PDF)

November 16, 2017

Eliminating Dependent Pattern Matching

Healfdene Goguen, Conor McBride and James McKinna. Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday: 521—540 (2006)

Paper (PDF)

October 12, 2017

Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity

Andreas M. Abel and Brigitte Pientka. Proc. of ICFP: 185—196 (2013)

Paper (PDF)

September 28, 2017

Programming with ornaments

Hsiang-Shang Ko and Jeremy Gibbons. Journal of Functional Programming 27 (2016)

Paper (PDF)

September 21, 2017

Representing Control: a Study of the CPS Transformation

Oliver Danvy and Andrzex Filinski. Mathematical Structures in Computer Science 2(4) (1992)

Paper (PDF)

September 14, 2017

The Duality of Construction

Paul Downen and Zena M. Ariola. Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410: 249—269 (2014)

Paper (PDF)

July 13, 2017

Classes and Mixins

Matthew Flatt, Shriram Krishnamurthi and Matthias Felleisen. Proc. of POPL: 171—183 (1998)

Paper (PDF)

June 8, 2017

Introducing a Calculus of Effects and Handlers for Natural Language Semantics

Jirka Maršík and Maxime Amblard. Formal Grammar : 20th and 21st International Conferences, FG 2015, Barcelona, Spain, August 2015, Revised Selected Papers. FG 2016, Bozen, Italy, August 2016, Proceedings: 257—272 (2016)

Paper (PDF)

June 1, 2017

Feature-Oriented Programming with Object Algebras

Bruno C. d. S. Oliveira, Tijs van der Storm, Alex Loh and William R. Cook. Proc. of ECOOP: 27—51 (2013)

Paper (PDF)

May 18, 2017

Shift to control

Chung-chieh Shan. Proc. of Scheme Workshop: 99—107 (2004)

Paper (PDF)

May 3, 2017

Generalizing Inference Systems by Coaxioms

Davide Ancona, Francesco Dagnino and Elena Zucca. Proc. of ESOP: 29—55 (2017)

Paper (PDF)

April 5, 2017

Objects and Classes, Co-algebraically

Bart Jacobs. Object Orientation with Parallelism and Persistence: 83—103 (1996)

Paper (PDF)

March 29, 2017

The expression lemma

Ralf Lämmel and Ondrej Rypacek. Proc. of MPC (2008)

Paper (PDF)

March 22, 2017

Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines

Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand and Saman Amarasinghe. Proc. of PLDI: 519—530 (2013)

Paper (PDF)

March 1, 2017

Do Be Do Be Do

Sam Lindley, Conor McBride and Craig McLaughlin. Proc. of POPL: 500—514 (2017)

Paper (PDF)

February 15, 2017

Staging Generic Programming

Jeremy Yallop. Proc. of PEPM: 85—96 (2016)

Paper (PDF)

February 8, 2017

Farms, Pipes, Streams and Reforestation: Reasoning About Structured Parallel Processes Using Types and Hylomorphisms

David Castro, Kevin Hammond and Susmit Sarkar. Proc. of ICFP: 4—17 (2016)

Paper (PDF)

February 1, 2017

Focusing on Pattern Matching

Neelakantan R. Krishnaswami. Proc. of POPL: 366—378 (2009)

Paper (PDF)

January 25, 2017

Beta Reduction is Invariant, Indeed

Beniamino Accattoli and Ugo Dal Lago. Proc. of CSL-LICS (2014)

Paper (PDF)

January 18, 2017

Generating Performance Portable Code Using Rewrite Rules: From High-level Functional Expressions to High-performance OpenCL Code

Michel Steuwer, Christian Fensch, Sam Lindley and Christophe Dubach. Proc. of ICFP: 205—217 (2015)

Paper (PDF)

December 14, 2016

Stream Fusion, to Completenes

Smaragdakis Kiselyov, Biboudis, Palladinos. Proc. of POPL (2017)

Paper (PDF)

December 7, 2016

seL4: Formal Verification of an OS Kernel

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood. Proc. of SOSP: 207—220 (2009)

Paper (PDF)

November 30, 2016

DART: Directed Automated Random Testing

Patrice Godefroid, Nils Klarlund and Koushik Sen. Proc. of PLDI: 213—223 (2005)

Paper (PDF)

November 16, 2016

Difficulties in Learning Inheritance and Polymorphism

Neomi Liberman, Catriel Beeri and Yifat Ben-David Kolikant. ACM TOCE (Transactions on Computing Education) 11(1) (2011)

Paper (PDF)

November 7, 2016

Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)

Christos Dimoulas, Max S. New, Robert Bruce Findler and Matthias Felleisen. Proc. of ICFP: 117—131 (2016)

Paper (PDF)

October 24, 2016

A Virtual Class Calculus (Extended Version)

Erik Ernst, Klaus Ostermann and William R. Cook. Proc. of POPL: 270—282 (2006)

Paper (PDF)

October 17, 2016

The Constrained-monad Problem

Neil Sculthorpe, Jan Bracker, George Giorgidze and Andy Gill. Proc. of ICFP: 287—298 (2013)

Paper (PDF)

October 10, 2016

Does Homotopy Type Theory Provide a Foundation for Mathematics?

James Ladyman and Stuart Presnell. The British Journal for the Philosophy of Science (2016)

Paper (PDF)

September 26, 2016

The Essence of Multi-stage Evaluation in LMS

Tiark Rompf. In: A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday: 318—335 (2016)

Paper (PDF)

September 19, 2016

Can Programming Be Liberated from the Von Neumann Style? A Functional Style and Its Algebra of Programs

John Backus. Commun. ACM 21(8): 613—641 (1978)

Paper (PDF)

July 18, 2016

Mini-languages: a way to learn programming principles

Peter Brusilovsky, Eduardo Calabrese, Jozef Hvorecky, Anatoly Kouchnirenko and Philip Miller. Education and Information Technologies 2(1): 65—83 (1997)

Paper (PDF)

July 11, 2016

Complete and Decidable Type Inference for GADTs

Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann and Dimitrios Vytiniotis. Proc. of ICFP: 341—352 (2009)

This link has a version later than the proceedings, so please use this.

Paper (PDF)

July 4, 2016

Types As Intervals

Robert Cartwright. Proc. of POPL: 22—36 (1985)

Paper (PDF)

June 27, 2016

Arrows, Robots, and Functional Reactive Programming

Paul Hudak, Antony Courtney, Henrik Nilsson and John Peterson. In: Advanced Functional Programming (AFP): 4th International School, 2002. Revised Lectures: 159—187 (2003)

Paper (PDF)

June 6, 2016

The Essence of Dependent Object Types

Nada Amin, Karl Samuel Grütter, Martin Odersky, Tiark Rompf and Sandro Stucki. Proc. of WadlerFest (2016)

Paper (PDF)

May 23, 2016

Everything Old is New Again: Quoted Domain-specific Languages

Shayan Najd, Sam Lindley, Josef Svenningsson and Philip Wadler. Proc. of PEPM: 25—36 (2016)

Paper (PDF)

May 9, 2016

The Design and Implementation of a Verification Technique for GPU Kernels

Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson and John Wickerson. ACM Trans. Program. Lang. Syst. 37(3) (2015)

We'll discuss Sec. 2+3 only (14 pages).

Paper (PDF)

March 16, 2016

Evaluation of Games for Teaching Computer Science

Ben Gibson and Tim Bell. Proc. of 8th Workshop in Primary and Secondary Computing Education: 51—60 (2013)

Paper (PDF)

March 9, 2016

Lightweight implementations of probabilistic programming languages via transformational compilation

David Wingate, Andreas Stuhlmueller and Noah D. Goodman. International Conference on Artificial Intelligence and Statistics: 770—778 (2011)

Paper (PDF)

March 2, 2016

Guarded Recursive Datatype Constructors

Hongwei Xi, Chiyan Chen and Gang Chen. Proc. of POPL: 224—235 (2003)

Paper (PDF)

February 17, 2016

Modularity and Implementation of Mathematical Operational Semantics

Mauro Jaskelioff, Neil Ghani and Graham Hutton. Proc. of Mathematically Structured Functional Programming (2008)

Paper (PDF)

February 10, 2016

Freer Monads, More Extensible Effects

Oleg Kiselyov and Hiromi Ishii. Proc. of Haskell Symposium: 94—105 (2015)

Paper (PDF)

January 27, 2016

Managing the development of large software systems: Concepts and techniques

W. W. Royce. Technical Papers of Western Electronic Show and Convention (WesCon) (1970)

This paper introduced the waterfall model of software development.

Paper (PDF)

January 20, 2016

Copy and Paste Redeemed

Krishna Narasimhan and Christoph Reichenbach. Proc. of ASE (2015)

Paper (PDF)

December 16, 2015

Stochastic Lambda Calculus and Monads of Probability Distributions

Norman Ramsey and Avi Pfeffer. Proc. of POPL: 154—165 (2002)

Paper (PDF)

December 9, 2015

Polymorphic Typed Defunctionalization

François Pottier and Nadji Gauthier. Proc. of POPL: 89—98 (2004)

Paper (PDF)

November 25, 2015

Functional Programming with Structured Graphs

Bruno C.d.S. Oliveira and William R. Cook. Proc. of ICFP: 77—88 (2012)

Paper (PDF)

November 18, 2015

F-ing Modules

Andreas Rossberg, Claudio V. Russo and Derek Dreyer. Proc. of TLDI: 89—102 (2010)

Paper (PDF)

November 4, 2015

Monad Transformers and Modular Interpreters

Sheng Liang, Paul Hudak and Mark Jones. Proc. of POPL: 333—343 (1995)

Paper (PDF)

October 28, 2015

A dissection of L

Arnaud Spiwack (2014)

We will skip Sec. 5.

Paper (PDF)

October 21, 2015

Resource-Safe Systems Programming with Embedded Domain Specific Languages

Edwin Brady and Kevin Hammond. Proc. of PADL: 242—257 (2012)

Paper (PDF)

October 14, 2015

Semantics of context-free languages

Donald E. Knuth. Mathematical systems theory 2(2): 127—145 (1968)

Paper (PDF)

October 5, 2015

Monads for Functional Programming

Philip Wadler. Advanced Functional Programming, Spring School: 24—52 (1995)

Paper (PDF)

September 28, 2015

Cross-Language Code Analysis and Refactoring

P. Mayer and A. Schroeder. Proc. of Source Code Analysis and Manipulation (SCAM): 94—103 (2012)

Paper (PDF)

September 21, 2015

Selective Memoization

Umut A. Acar, Guy E. Blelloch and Robert Harper. Proc. of POPL: 14—25 (2003)

Paper (PDF)

July 20, 2015

Packrat Parsers Can Support Left Recursion

Alessandro Warth, James R. Douglass and Todd Millstein. Proc. of PEPM: 103—110 (2008)

Paper (PDF)

July 13, 2015

Combinators for Bi-directional Tree Transformations: A Linguistic Approach to the View Update Problem

J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce and Alan Schmitt. Proc. of POPL: 233—246 (2005)

Paper (PDF)

June 29, 2015

To CNF or not to CNF? An efficient yet presentable version of the CYK algorithm

Martin Lange and Hans Leiß. Informatica Didactica 8: 2008—2010 (2009)

Paper (PDF)

June 22, 2015

Embedded Probabilistic Programming

Oleg Kiselyov and Chung-Chieh Shan. IFIP TC 2 Working Conference on Domain-Specific Languages: 360—384 (2009)

Additional resources available at

Paper (PDF)

June 15, 2015

An Empirical Study of Regression Testing Techniques Incorporating Context and Lifetime Factors and Improved Cost-benefit Models

Hyunsook Do and Gregg Rothermel. 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering: 141—151 (2006)

Paper (PDF)

June 8, 2015

Towards a theory of type structure

John C. Reynolds. Programming Symposium: 408—425 (1974)

This is the paper that introduced System F.

Paper (PDF)

May 18, 2015

A Generic Account of Continuation-passing Styles

John Hatcliff and Olivier Danvy. Proc. of POPL: 458—471 (1994)

Paper (PDF)

May 11, 2015

A Denotational Semantics of Inheritance and Its Correctness

W. Cook and J. Palsberg. Proc. of OOPSLA: 433—443 (1989)

Paper (PDF)

May 4, 2015

Pattern matching without K

Jesper Cockx, Dominique Devriese and Frank Piessens. Proc. of ICFP: 257—268 (2014)

You should jump over Sec. 3 (the correctness proof) if you get stuck.

Paper (PDF)

April 27, 2015

Polytypic values possess polykinded types

Ralf Hinze. Mathematics of Program Construction: 2—27 (2000)

We will read sections 1–5. Timeslot: 16:00-17:00.

Paper (PDF)

April 13, 2015

Subject-oriented Programming: A Critique of Pure Objects

William Harrison and Harold Ossher. Proc. of OOPSLA: 411—428 (1993)

We will only discuss sections 1-6. Timeslot: 15:00-16:00.

Paper (PDF)

March 25, 2015

Points-to Analysis in Almost Linear Time

Bjarne Steensgaard. Proc. of POPL: 32—41 (1996)

Paper (PDF)

March 18, 2015

Codatatypes in ML

Tatsuya Hagino. Journal of Symbolic Computation 8(6): 629—650 (1989)

Paper (PDF)

March 11, 2015

Comparing object encodings

Kim B. Bruce, Luca Cardelli and Benjamin C. Pierce. Theoretical Aspects of Computer Software: 415—438 (1997)

Paper (PDF)

March 4, 2015

On the criteria to be used in decomposing systems into modules

David L. Parnas. Commun. ACM 15(12): 1053—1058 (1972)

Paper (PDF)

February 25, 2015

The Essence of the Iterator Pattern

Jeremy Gibbons and Bruno C. d. S. Oliveira. J. Funct. Program. 19(3-4): 377—402 (2009)

Paper (PDF)

February 18, 2015

Local Reasoning about Programs that Alter Data Structures

Peter O'Hearn, John Reynolds and Hongseok Yang. Workshop on Computer Science Logic: 1—19 (2001)

This is the paper that introduced separation logic, a very influential and useful variant of Hoare logic.

Paper (PDF)

February 11, 2015

An axiomatic basis for computer programming

C. A. R. Hoare. Commun. ACM 12(10): 576—580 (1969)

This is the paper that introduced Hoare logic.

Paper (PDF)