POPL

Publications

2017

Carlo Angiuli, Robert Harper, Todd Wilson
Computational higher-dimensional type theory. POPL (2017)
Andrej Dudenhefner, Jakob Rehof
Intersection type calculi of bounded dimension. POPL (2017)
Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps
Component-based synthesis for complex APIs. POPL (2017)
Jochen Hoenicke, Rupak Majumdar, Andreas Podelski
Thread modularity at many levels: a pearl in compositional verification. POPL (2017)
Danko Ilik
The exp-log normal form of types: decomposing extensional equality and representing terms compactly. POPL (2017)
Stephanie Weirich
The influence of dependent types (keynote). POPL (2017)
Loris D'Antoni, Margus Veanes
Monadic second-order logic on finite sequences. POPL (2017)
Nada Amin, Tiark Rompf
LMS-Verify: abstraction without regret for verified systems programming. POPL (2017)
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 POPL (2017)
Kimball Germane, Matthew Might
A posteriori environment analysis with Pushdown Delta CFA. POPL (2017)
Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, Xavier Rival
Semantic-directed clumping of disjunctive abstract states. POPL (2017)
Aaron Turon
Rust: from POPL to practice (keynote). POPL (2017)
Robbert Krebbers, Amin Timany, Lars Birkedal
Interactive proofs in higher-order concurrent separation logic. POPL (2017)
Qirun Zhang, Zhendong Su
Context-sensitive data-dependence analysis via linear conjunctive language reachability. POPL (2017)
Gabriel Scherer
Deciding equivalence with sums and the empty type. POPL (2017)
John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides
Automatically comparing memory consistency models. POPL (2017)
Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel
Hypercollecting semantics and its application to static analysis of information flow. POPL (2017)
Stephen Chang, Alex Knauth, Ben Greenman
Type systems as macros. POPL (2017)
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
Dijkstra monads for free. POPL (2017)
Laura Kovács, Simon Robillard, Andrei Voronkov
Coming to terms with quantified reasoning. POPL (2017)
Khurram A. Jafery, Jana Dunfield
Sums of uncertainty: refinements go gradual. POPL (2017)
Stephen Dolan, Alan Mycroft
Polymorphism, subtyping, and type inference in MLsub. POPL (2017)
Jan Hoffmann, Ankush Das, Shu-Chun Weng
Towards automatic resource bound analysis for OCaml. POPL (2017)
Christopher Lidbury, Alastair F. Donaldson
Dynamic race detection for C++11. POPL (2017)
Ziv Scully, Adam Chlipala
A program optimization for automatic database result caching. POPL (2017)
Mingsheng Ying, Shenggang Ying, Xiaodi Wu
Invariants of quantum programs: characterisations and generation. POPL (2017)
Eryk Kopczynski, Szymon Torunczyk
LOIS: syntax and semantics. POPL (2017)
Akhilesh Srikanth, Burak Sahin, William R. Harris
Complexity verification using guided theorem enumeration. POPL (2017)
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva
Cantor meets scott: semantic foundations for probabilistic networks. POPL (2017)
Nada Amin, Tiark Rompf
Type soundness proofs with definitional interpreters. POPL (2017)
Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, Zvonimir Rakamaric
Rigorous floating-point mixed-precision tuning. POPL (2017)
Michael M. Vitousek, Cameron Swords, Jeremy G. Siek
Big types in little runtime: open-world soundness and collaborative blame for gradual type systems. POPL (2017)
Taro Sekiyama, Atsushi Igarashi
Stateful manifest contracts. POPL (2017)
Sam Lindley, Conor McBride, Craig McLaughlin
Do be do be do. POPL (2017)
Karl Crary
Modules, abstraction, and parametric polymorphism. POPL (2017)
Daan Leijen
Type directed compilation of row-typed algebraic effects. POPL (2017)
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann
Relational cost analysis. POPL (2017)
Radu Grigore
Java generics are turing complete. POPL (2017)
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
A promising semantics for relaxed-memory concurrency. POPL (2017)
Chung-chieh Shan, Norman Ramsey
Exact Bayesian inference by symbolic disintegration. POPL (2017)
Lucas Brutschy, Dimitar K. Dimitrov, Peter Müller, Martin T. Vechev
Serializability for eventual consistency: criterion, analysis, and applications. POPL (2017)
Matteo Cimini, Jeremy G. Siek
Automatically generating the dynamic semantics of gradually typed languages. POPL (2017)
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Coupling proofs are probabilistic product programs. POPL (2017)
Gagandeep Singh, Markus Püschel, Martin T. Vechev
Fast polyhedra abstract domain. POPL (2017)
Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida
Fencing off go: liveness and safety for channel-based programming. POPL (2017)
Ugo Dal Lago, Claudia Faggian, Benoît Valiron, Akira Yoshimizu
The geometry of parallelism: classical, probabilistic, and quantum effects. POPL (2017)
Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak
Contract-based resource verification for higher-order functions with memoization. POPL (2017)
Danfeng Zhang, Daniel Kifer
LightDP: towards automating differential privacy proofs. POPL (2017)
Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal
A relational model of types-and-effects in higher-order concurrent separation logic. POPL (2017)
Jennifer Paykin, Robert Rand, Steve Zdancewic
QWIRE: a core language for quantum circuits. POPL (2017)