Compiler Design Lab

Programming Language Implementation Seminar

In this seminar, we read recent papers from the top conferences and journals in programming languages. Topics include: program analysis, program optimization, program synthesis, compilation.

People

Sebastian Hack, Jan Reineke, Johannes Doerfert, Simon Moll

Organization

Please register to the forum to follow this seminar and interact with you fellow students.

Language English
Participants 12 / 12 (seats taken / maximum seats)
Waiting list 2 (please attend the Preparatory Meeting)
Preparatory Meeting 2015-10-21, 16:00 - 18:00 pm (cum tempore), E1.3 room 401
Weekly Meeting Wednesdays, 16:00 - 18:00 pm (cum tempore), E1.3 room 401
Prerequisites Preferably, you take part or have taken part in the compiler construction course.
Topics Recent papers from programming languages, program analysis, program synthesis, compilers

Registration

Write a mail to Johannes Doerfert until 2015-10-20 and come to the preparatory meeting.

Modus Operandi

Each paper will be assigned to one participant. We will have weekly meetings during the semester in which we will discuss one of the papers. The discussion will be managed by the student to whom the paper was assigned. She/he is responsible for giving a short summary on the paper and for structuring the following discussion.

Every week each student has to write a summary (max. 500 words) on the week's paper. This summary should include open questions and is to be submitted two days before the corresponding meeting (11:59 noon). The summaries of all participants will be made available and can be used by the moderator to structure the discussion in the following meeting.

At the end of the semester each participant will give a presentation (30 minutes) about her/his paper.

Each participant is allowed to drop two summaries without any particular reason. In case you drop a summary, please send a short mail telling so.

Once registered, you cannot unregister later than 2015-10-23.

Dates

Sessions

Date Moderator Paper Summaries
2015-11-18Sebastian Meyer M3
2015-11-25Tatiana DembelovaM4
2015-12-02Fanyu Ye O1
2015-12-09Bran Hagger O2
2015-12-16Wiam Rachid O4
2016-01-06Tina Jung S1
2016-01-13Fabian Ritter S2
2016-01-20Gereon Fox S3
2016-01-27Lukasz HanuszczakS4
2016-02-03Heiko Becker V1

Final Talks

Papers

[V] Compiler Correctness, Translation Validation, Self Composition

  1. Gilles Barthe, Juan Manuel Crespo, César Kunz:
    Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. LFCS 2013: 29-43
  2. Nuno P. Lopes, David Menendez, Santosh Nagarakatte, John Regehr:
    Provably correct peephole optimizations with alive. PLDI 2015: 22-32
  3. Rahul Sharma, Eric Schkufza, Berkeley R. Churchill, Alex Aiken:
    Data-driven equivalence checking. OOPSLA 2013: 391-406
  4. Kedar S. Namjoshi, Lenore D. Zuck:
    Witnessing Program Transformations. SAS 2013: 304-323

[S] Program Synthesis

  1. Dimitrios Prountzos, Roman Manevich, Keshav Pingali:
    Synthesizing parallel graph programs via automated planning. PLDI 2015: 533-544
  2. Venkatesh Srinivasan, Thomas W. Reps:
    Synthesis of machine code from semantics. PLDI 2015: 596-607
  3. Eric Schkufza, Rahul Sharma, Alex Aiken:
    Stochastic superoptimization. ASPLOS 2013: 305-316
  4. John Feser, Swarat Chaudhuri, Isil Dillig:
    Synthesizing Data Structure Transformations from Input-Output Examples. PLDI 2015
  5. Robert A Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar, Margus Veanes:
    Program Boosting: Program Synthesis via Crowd-Sourcing. POPL 2015

[O] Code Optimization

  1. Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock:
    Automatically improving accuracy for floating point expressions. PLDI 2015: 1-11
  2. Thomas Würthinger, Christian Wimmer, Andreas Wöß, Lukas Stadler, Gilles Duboscq, Christian Humer, Gregor Richards, Doug Simon, Mario Wolczko:
    One VM to rule them all. Onward! 2013: 187-204
  3. Ramakrishna Upadrasta, Albert Cohen:
    Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra. POPL 2013: 483-496
  4. Tobias Grosser, Sven Verdoolaege, Albert Cohen:
    Polyhedral AST Generation Is More Than Scanning Polyhedra TOPLAS 2015

[C] Concurrency

  1. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber:
    Mathematizing C++ concurrency. POPL 2011: 55-66
  2. Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli:
    Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. POPL 2015: 209-220

[M] Misc

  1. Adam Chlipala:
    Ur/Web: A Simple Model for Programming the Web. POPL 2015: 153-165
  2. Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock:
    Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. OSDI 2014: 33-47
  3. Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie:
    A Formally-Verified C Static Analyzer. POPL 2015: 247-259
  4. Ben Greenman, Fabian Muehlboeck, Ross Tate:
    Getting F-Bounded Polymorphism into Shape. PLDI 2014: 89-99
  5. Quentin Carbonneaux, Jan Hoffmann, Zhong Shao:
    Compositional Certified Resource Bounds. PLDI 2015