List of POPL 2017 papers with crowd-sourced preprint links

https://github.com/gasche/popl2017-papers/ has a list of POPL 2017 papers with crowd-sourced links to the preprints. The deadline for camera-ready version (a version provided by the researchers that takes reviewers' comment into account) is only on November 7th, so one should expect more preprints to be available after that.

Feel free to mention any paper that catches your interest. If you are very curious in a particular work that does not have an online preprint, sending an email to the authors to ask them whether they plan to have a preprint accessible online can help a lot.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Amazing work as always!


What stands out to you?

What stands out to you?

Just based on the titles and

Just based on the titles and descriptions?

  • Computational Higher-Dimensional Type Theory
  • Hazelnut: A Bidirectionally Typed Structure Editor Calculus
  • Exact Bayesian Inference by Symbolic Disintegration
  • Type Directed Compilation of Row-Typed Algebraic Effects / Do be do be do
  • A Posteriori Environment Analysis with Pushdown Delta CFA
  • Beginner's Luck: A Language for Property-Based Generators
  • Thanks, Hazelnut looks

    Thanks, Hazelnut looks interesting, but I still have trouble figuring out how to turn theory into profit.

    The biggest win is that

    ...bidirectionality gives them a really elegant/pretty story for holes nested in holes. This lets them evade one of the traditional pitfalls of syntax editors, namely that programs must be written in a top-down style.

    Eg, if you are in a hole context where (say) a string is expected, and you write the number 5, their structure editor doesn't ban this. Instead, it puts the 5 inside a nested hole, so that you can later refine the bit of program that eats the 5 to make the string.

    You can download a (very) toy implementation on Github. It's a very direct implementation of the theory, so it feels like someone pasted an HTML5 interface over the Cornell Program Synthesizer, but it's enough to get the ideas in the paper across.

    toy implementation

    You can play with our reference implementation here. (The preprint+Agda mechanization is also linked from there)

    (ignore)

    (posted in the wrong place)