POPL 2017 – Author Index

A B C D E F G H I J K L M N O P R S T V W X Y Z

	Ahman, Danel	POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Akella, Aditya	POPL '17: "Genesis: Synthesizing Forwarding ..." Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks Kausik Subramanian, Loris D'Antoni, and Aditya Akella (University of Wisconsin-Madison, USA) @InProceedings{POPL17p839, author = {Kausik Subramanian and Loris D'Antoni and Aditya Akella}, title = {Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {839-838}, doi = {}, year = {2017}, } Article: popl17main-main35-p (type: Full Paper) doi:
	Aldrich, Jonathan	POPL '17: "Hazelnut: A Bidirectionally ..." Hazelnut: A Bidirectionally Typed Structure Editor Calculus Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer (Carnegie Mellon University, USA; Oregon State University, USA; University of Colorado at Boulder, USA) @InProceedings{POPL17p295, author = {Cyrus Omar and Ian Voysey and Michael Hilton and Jonathan Aldrich and Matthew A. Hammer}, title = {Hazelnut: A Bidirectionally Typed Structure Editor Calculus}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {295-294}, doi = {}, year = {2017}, } Article: popl17main-main319-p (type: Full Paper) doi:
	Alglave, Jade	POPL '17: "Ogre and Pythia: An Invariance ..." Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models Jade Alglave and Patrick Cousot (Microsoft Research, UK; University College London, UK; New York University, USA; ENS, France) @InProceedings{POPL17p199, author = {Jade Alglave and Patrick Cousot}, title = {Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {199-198}, doi = {}, year = {2017}, } Article: popl17main-main232-p (type: Full Paper) doi:
	Amin, Nada	POPL '17: "LMS-Verify: Abstraction without ..." LMS-Verify: Abstraction without Regret for Verified Systems Programming Nada Amin and Tiark Rompf (EPFL, Switzerland; Purdue University, USA) @InProceedings{POPL17p1175, author = {Nada Amin and Tiark Rompf}, title = {LMS-Verify: Abstraction without Regret for Verified Systems Programming}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1175-1174}, doi = {}, year = {2017}, } Article: popl17main-main144-p (type: Full Paper) doi: POPL '17: "Type Soundness Proofs with ..." Type Soundness Proofs with Definitional Interpreters Nada Amin and Tiark Rompf (EPFL, Switzerland; Purdue University, USA) @InProceedings{POPL17p951, author = {Nada Amin and Tiark Rompf}, title = {Type Soundness Proofs with Definitional Interpreters}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {951-950}, doi = {}, year = {2017}, } Article: popl17main-main143-p (type: Full Paper) doi:
	Angiuli, Carlo	POPL '17: "Computational Higher-Dimensional ..." Computational Higher-Dimensional Type Theory Carlo Angiuli, Robert Harper, and Todd Wilson (Carnegie Mellon University, USA; California State University at Fresno, USA) @InProceedings{POPL17p967, author = {Carlo Angiuli and Robert Harper and Todd Wilson}, title = {Computational Higher-Dimensional Type Theory}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {967-966}, doi = {}, year = {2017}, } Article: popl17main-main126-p (type: Full Paper) doi:
	Assaf, Mounir	POPL '17: "Hypercollecting Semantics ..." Hypercollecting Semantics and Its Application to Static Analysis of Information Flow Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel (Stevens Institute of Technology, USA; CEA LIST, France; CentraleSupélec, France) @InProceedings{POPL17p1191, author = {Mounir Assaf and David A. Naumann and Julien Signoles and Éric Totel and Frédéric Tronel}, title = {Hypercollecting Semantics and Its Application to Static Analysis of Information Flow}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1191-1190}, doi = {}, year = {2017}, } Article: popl17main-main256-p (type: Full Paper) doi:
	Azevedo de Amorim, Arthur	POPL '17: "A Semantic Account of Metric ..." A Semantic Account of Metric Preservation Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui (University of Pennsylvania, USA; SUNY Buffalo, USA; Kyoto University, Japan; ENS, France) @InProceedings{POPL17p807, author = {Arthur Azevedo de Amorim and Marco Gaboardi and Justin Hsu and Shin-ya Katsumata and Ikram Cherigui}, title = {A Semantic Account of Metric Preservation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {807-806}, doi = {}, year = {2017}, } Article: popl17main-main259-p (type: Full Paper) doi:
	Baranowski, Mark	POPL '17: "Rigorous Floating-Point Mixed-Precision ..." Rigorous Floating-Point Mixed-Precision Tuning Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić (University of Utah, USA) @InProceedings{POPL17p535, author = {Wei-Fan Chiang and Mark Baranowski and Ian Briggs and Alexey Solovyev and Ganesh Gopalakrishnan and Zvonimir Rakamarić}, title = {Rigorous Floating-Point Mixed-Precision Tuning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {535-534}, doi = {}, year = {2017}, } Article: popl17main-main41-p (type: Full Paper) doi:
	Barthe, Gilles	POPL '17: "Coupling Proofs Are Probabilistic ..." Coupling Proofs Are Probabilistic Product Programs Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; Inria, France; University of Pennsylvania, USA; École Polytechnique, France) @InProceedings{POPL17p375, author = {Gilles Barthe and Benjamin Grégoire and Justin Hsu and Pierre-Yves Strub}, title = {Coupling Proofs Are Probabilistic Product Programs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {375-374}, doi = {}, year = {2017}, } Article: popl17main-main290-p (type: Full Paper) doi: POPL '17: "Relational Cost Analysis ..." Relational Cost Analysis Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann (MPI-SWS, Germany; IMDEA Software Institute, Spain; SUNY Buffalo, USA; Carnegie Mellon University, USA) @InProceedings{POPL17p551, author = {Ezgi Çiçek and Gilles Barthe and Marco Gaboardi and Deepak Garg and Jan Hoffmann}, title = {Relational Cost Analysis}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {551-550}, doi = {}, year = {2017}, } Article: popl17main-main107-p (type: Full Paper) doi:
	Batty, Mark	POPL '17: "Automatically Comparing Memory ..." Automatically Comparing Memory Consistency Models John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides (Imperial College London, UK; University of Kent, UK) @InProceedings{POPL17p407, author = {John Wickerson and Mark Batty and Tyler Sorensen and George A. Constantinides}, title = {Automatically Comparing Memory Consistency Models}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {407-406}, doi = {}, year = {2017}, } Article: popl17main-main2-p (type: Full Paper) doi: POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Berenger, Francois	POPL '17: "Semantic-Directed Clumping ..." Semantic-Directed Clumping of Disjunctive Abstract States Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival (Inria, France; CNRS, France; ENS, France; University of Colorado at Boulder, USA) @InProceedings{POPL17p231, author = {Huisong Li and Francois Berenger and Bor-Yuh Evan Chang and Xavier Rival}, title = {Semantic-Directed Clumping of Disjunctive Abstract States}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {231-230}, doi = {}, year = {2017}, } Article: popl17main-main220-p (type: Full Paper) doi:
	Biboudis, Aggelos	POPL '17: "Stream Fusion, to Completeness ..." Stream Fusion, to Completeness Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, and Yannis Smaragdakis (Tohoku University, Japan; University of Athens, Greece; Nessos IT, Greece) @InProceedings{POPL17p519, author = {Oleg Kiselyov and Aggelos Biboudis and Nick Palladinos and Yannis Smaragdakis}, title = {Stream Fusion, to Completeness}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {519-518}, doi = {}, year = {2017}, } Article: popl17main-main218-p (type: Full Paper) doi:
	Birkedal, Lars	POPL '17: "Interactive Proofs in Higher-Order ..." Interactive Proofs in Higher-Order Concurrent Separation Logic Robbert Krebbers, Amin Timany, and Lars Birkedal (Delft University of Technology, Netherlands; KU Leuven, Belgium; Aarhus University, Denmark) @InProceedings{POPL17p423, author = {Robbert Krebbers and Amin Timany and Lars Birkedal}, title = {Interactive Proofs in Higher-Order Concurrent Separation Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, } Article: popl17main-main99-p (type: Full Paper) doi: POPL '17: "A Relational Model of Types-and-Effects ..." A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal (Aarhus University, Denmark; University of Cambridge, UK) @InProceedings{POPL17p439, author = {Morten Krogh-Jespersen and Kasper Svendsen and Lars Birkedal}, title = {A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {439-438}, doi = {}, year = {2017}, } Article: popl17main-main192-p (type: Full Paper) doi:
	Blelloch, Guy E.	POPL '17: "Parallel Functional Arrays ..." Parallel Functional Arrays Ananya Kumar, Guy E. Blelloch, and Robert Harper (Carnegie Mellon University, USA) @InProceedings{POPL17p999, author = {Ananya Kumar and Guy E. Blelloch and Robert Harper}, title = {Parallel Functional Arrays}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {999-998}, doi = {}, year = {2017}, } Article: popl17main-main157-p (type: Full Paper) doi:
	Bouajjani, Ahmed	POPL '17: "On Verifying Causal Consistency ..." On Verifying Causal Consistency Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza (University of Paris Diderot, France; EPFL, Switzerland; Inria, France) @InProceedings{POPL17p903, author = {Ahmed Bouajjani and Constantin Enea and Rachid Guerraoui and Jad Hamza}, title = {On Verifying Causal Consistency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {903-902}, doi = {}, year = {2017}, } Article: popl17main-main255-p (type: Full Paper) doi:
	Briggs, Ian	POPL '17: "Rigorous Floating-Point Mixed-Precision ..." Rigorous Floating-Point Mixed-Precision Tuning Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić (University of Utah, USA) @InProceedings{POPL17p535, author = {Wei-Fan Chiang and Mark Baranowski and Ian Briggs and Alexey Solovyev and Ganesh Gopalakrishnan and Zvonimir Rakamarić}, title = {Rigorous Floating-Point Mixed-Precision Tuning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {535-534}, doi = {}, year = {2017}, } Article: popl17main-main41-p (type: Full Paper) doi:
	Brown, Matt	POPL '17: "Typed Self-Evaluation via ..." Typed Self-Evaluation via Intensional Type Functions Matt Brown and Jens Palsberg (University of California at Los Angeles, USA) @InProceedings{POPL17p663, author = {Matt Brown and Jens Palsberg}, title = {Typed Self-Evaluation via Intensional Type Functions}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {663-662}, doi = {}, year = {2017}, } Article: popl17main-main96-p (type: Full Paper) doi:
	Bruse, Florian	POPL '17: "On the Relationship between ..." On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic Naoki Kobayashi, Étienne Lozes, and Florian Bruse (University of Tokyo, Japan; ENS, France; CNRS, France; University of Kassel, Germany) @InProceedings{POPL17p471, author = {Naoki Kobayashi and Étienne Lozes and Florian Bruse}, title = {On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {471-470}, doi = {}, year = {2017}, } Article: popl17main-main97-p (type: Full Paper) doi:
	Brutschy, Lucas	POPL '17: "Serializability for Eventual ..." Serializability for Eventual Consistency: Criterion, Analysis, and Applications Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev (ETH Zurich, Switzerland) @InProceedings{POPL17p711, author = {Lucas Brutschy and Dimitar Dimitrov and Peter Müller and Martin Vechev}, title = {Serializability for Eventual Consistency: Criterion, Analysis, and Applications}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {711-710}, doi = {}, year = {2017}, } Article: popl17main-main285-p (type: Full Paper) doi:
	Chang, Bor-Yuh Evan	POPL '17: "Semantic-Directed Clumping ..." Semantic-Directed Clumping of Disjunctive Abstract States Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival (Inria, France; CNRS, France; ENS, France; University of Colorado at Boulder, USA) @InProceedings{POPL17p231, author = {Huisong Li and Francois Berenger and Bor-Yuh Evan Chang and Xavier Rival}, title = {Semantic-Directed Clumping of Disjunctive Abstract States}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {231-230}, doi = {}, year = {2017}, } Article: popl17main-main220-p (type: Full Paper) doi:
	Chang, Stephen	POPL '17: "Type Systems as Macros ..." Type Systems as Macros Stephen Chang, Alex Knauth, and Ben Greenman (Northeastern University, USA) @InProceedings{POPL17p983, author = {Stephen Chang and Alex Knauth and Ben Greenman}, title = {Type Systems as Macros}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {983-982}, doi = {}, year = {2017}, } Article: popl17main-main247-p (type: Full Paper) doi:
	Chatterjee, Krishnendu	POPL '17: "Stochastic Invariants for ..." Stochastic Invariants for Probabilistic Termination Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić (IST Austria, Austria; University of Cambridge, UK) @InProceedings{POPL17p359, author = {Krishnendu Chatterjee and Petr Novotný and Ðorđe Žikelić}, title = {Stochastic Invariants for Probabilistic Termination}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {359-358}, doi = {}, year = {2017}, } Article: popl17main-main182-p (type: Full Paper) doi:
	Cherigui, Ikram	POPL '17: "A Semantic Account of Metric ..." A Semantic Account of Metric Preservation Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui (University of Pennsylvania, USA; SUNY Buffalo, USA; Kyoto University, Japan; ENS, France) @InProceedings{POPL17p807, author = {Arthur Azevedo de Amorim and Marco Gaboardi and Justin Hsu and Shin-ya Katsumata and Ikram Cherigui}, title = {A Semantic Account of Metric Preservation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {807-806}, doi = {}, year = {2017}, } Article: popl17main-main259-p (type: Full Paper) doi:
	Chiang, Wei-Fan	POPL '17: "Rigorous Floating-Point Mixed-Precision ..." Rigorous Floating-Point Mixed-Precision Tuning Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić (University of Utah, USA) @InProceedings{POPL17p535, author = {Wei-Fan Chiang and Mark Baranowski and Ian Briggs and Alexey Solovyev and Ganesh Gopalakrishnan and Zvonimir Rakamarić}, title = {Rigorous Floating-Point Mixed-Precision Tuning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {535-534}, doi = {}, year = {2017}, } Article: popl17main-main41-p (type: Full Paper) doi:
	Chlipala, Adam	POPL '17: "A Program Optimization for ..." A Program Optimization for Automatic Database Result Caching Ziv Scully and Adam Chlipala (Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA) @InProceedings{POPL17p503, author = {Ziv Scully and Adam Chlipala}, title = {A Program Optimization for Automatic Database Result Caching}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {503-502}, doi = {}, year = {2017}, } Article: popl17main-main260-p (type: Full Paper) doi:
	Çiçek, Ezgi	POPL '17: "Relational Cost Analysis ..." Relational Cost Analysis Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann (MPI-SWS, Germany; IMDEA Software Institute, Spain; SUNY Buffalo, USA; Carnegie Mellon University, USA) @InProceedings{POPL17p551, author = {Ezgi Çiçek and Gilles Barthe and Marco Gaboardi and Deepak Garg and Jan Hoffmann}, title = {Relational Cost Analysis}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {551-550}, doi = {}, year = {2017}, } Article: popl17main-main107-p (type: Full Paper) doi:
	Cimini, Matteo	POPL '17: "Automatically Generating the ..." Automatically Generating the Dynamic Semantics of Gradually Typed Languages Matteo Cimini and Jeremy G. Siek (Indiana University, USA) @InProceedings{POPL17p1095, author = {Matteo Cimini and Jeremy G. Siek}, title = {Automatically Generating the Dynamic Semantics of Gradually Typed Languages}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1095-1094}, doi = {}, year = {2017}, } Article: popl17main-main134-p (type: Full Paper) doi:
	Constantinides, George A.	POPL '17: "Automatically Comparing Memory ..." Automatically Comparing Memory Consistency Models John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides (Imperial College London, UK; University of Kent, UK) @InProceedings{POPL17p407, author = {John Wickerson and Mark Batty and Tyler Sorensen and George A. Constantinides}, title = {Automatically Comparing Memory Consistency Models}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {407-406}, doi = {}, year = {2017}, } Article: popl17main-main2-p (type: Full Paper) doi:
	Cousot, Patrick	POPL '17: "Ogre and Pythia: An Invariance ..." Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models Jade Alglave and Patrick Cousot (Microsoft Research, UK; University College London, UK; New York University, USA; ENS, France) @InProceedings{POPL17p199, author = {Jade Alglave and Patrick Cousot}, title = {Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {199-198}, doi = {}, year = {2017}, } Article: popl17main-main232-p (type: Full Paper) doi:
	Crary, Karl	POPL '17: "Modules, Abstraction, and ..." Modules, Abstraction, and Parametric Polymorphism Karl Crary (Carnegie Mellon University, USA) @InProceedings{POPL17p311, author = {Karl Crary}, title = {Modules, Abstraction, and Parametric Polymorphism}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {311-310}, doi = {}, year = {2017}, } Article: popl17main-main264-p (type: Full Paper) doi:
	Dal Lago, Ugo	POPL '17: "The Geometry of Parallelism: ..." The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu (University of Bologna, Italy; Inria, France; CNRS, France; University of Paris Diderot, France; University of Paris-Saclay, France; University of Tokyo, Japan) @InProceedings{POPL17p1143, author = {Ugo Dal Lago and Claudia Faggian and Benoît Valiron and Akira Yoshimizu}, title = {The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1143-1142}, doi = {}, year = {2017}, } Article: popl17main-main113-p (type: Full Paper) doi:
	D'Antoni, Loris	POPL '17: "Monadic Second-Order Logic ..." Monadic Second-Order Logic on Finite Sequences Loris D'Antoni and Margus Veanes (University of Wisconsin-Madison, USA; Microsoft Research, USA) @InProceedings{POPL17p455, author = {Loris D'Antoni and Margus Veanes}, title = {Monadic Second-Order Logic on Finite Sequences}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {455-454}, doi = {}, year = {2017}, } Article: popl17main-main32-p (type: Full Paper) doi: POPL '17: "Genesis: Synthesizing Forwarding ..." Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks Kausik Subramanian, Loris D'Antoni, and Aditya Akella (University of Wisconsin-Madison, USA) @InProceedings{POPL17p839, author = {Kausik Subramanian and Loris D'Antoni and Aditya Akella}, title = {Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {839-838}, doi = {}, year = {2017}, } Article: popl17main-main35-p (type: Full Paper) doi:
	Das, Ankush	POPL '17: "Towards Automatic Resource ..." Towards Automatic Resource Bound Analysis for OCaml Jan Hoffmann, Ankush Das, and Shu-Chun Weng (Carnegie Mellon University, USA; Yale University, USA) @InProceedings{POPL17p599, author = {Jan Hoffmann and Ankush Das and Shu-Chun Weng}, title = {Towards Automatic Resource Bound Analysis for OCaml}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {599-598}, doi = {}, year = {2017}, } Article: popl17main-main17-p (type: Full Paper) doi:
	Dillig, Isil	POPL '17: "Component-Based Synthesis ..." Component-Based Synthesis for Complex APIs Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps (University of Texas at Austin, USA; University of Wisconsin-Madison, USA) @InProceedings{POPL17p871, author = {Yu Feng and Ruben Martins and Yuepeng Wang and Isil Dillig and Thomas W. Reps}, title = {Component-Based Synthesis for Complex APIs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {871-870}, doi = {}, year = {2017}, } Article: popl17main-main93-p (type: Full Paper) doi:
	Dimitrov, Dimitar	POPL '17: "Serializability for Eventual ..." Serializability for Eventual Consistency: Criterion, Analysis, and Applications Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev (ETH Zurich, Switzerland) @InProceedings{POPL17p711, author = {Lucas Brutschy and Dimitar Dimitrov and Peter Müller and Martin Vechev}, title = {Serializability for Eventual Consistency: Criterion, Analysis, and Applications}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {711-710}, doi = {}, year = {2017}, } Article: popl17main-main285-p (type: Full Paper) doi:
	Dolan, Stephen	POPL '17: "Polymorphism, Subtyping, and ..." Polymorphism, Subtyping, and Type Inference in MLsub Stephen Dolan and Alan Mycroft (University of Cambridge, UK) @InProceedings{POPL17p263, author = {Stephen Dolan and Alan Mycroft}, title = {Polymorphism, Subtyping, and Type Inference in MLsub}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {263-262}, doi = {}, year = {2017}, } Article: popl17main-main228-p (type: Full Paper) doi:
	Donaldson, Alastair F.	POPL '17: "Dynamic Race Detection for ..." Dynamic Race Detection for C++11 Christopher Lidbury and Alastair F. Donaldson (Imperial College London, UK) @InProceedings{POPL17p695, author = {Christopher Lidbury and Alastair F. Donaldson}, title = {Dynamic Race Detection for C++11}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {695-694}, doi = {}, year = {2017}, } Article: popl17main-main106-p (type: Full Paper) doi:
	Dreyer, Derek	POPL '17: "A Promising Semantics for ..." A Promising Semantics for Relaxed-Memory Concurrency Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) @InProceedings{POPL17p391, author = {Jeehoon Kang and Chung-Kil Hur and Ori Lahav and Viktor Vafeiadis and Derek Dreyer}, title = {A Promising Semantics for Relaxed-Memory Concurrency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {391-390}, doi = {}, year = {2017}, } Article: popl17main-main65-p (type: Full Paper) doi:
	Dudenhefner, Andrej	POPL '17: "Intersection Type Calculi ..." Intersection Type Calculi of Bounded Dimension Andrej Dudenhefner and Jakob Rehof (TU Dortmund, Germany) @InProceedings{POPL17p935, author = {Andrej Dudenhefner and Jakob Rehof}, title = {Intersection Type Calculi of Bounded Dimension}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {935-934}, doi = {}, year = {2017}, } Article: popl17main-main130-p (type: Full Paper) doi:
	Dunfield, Joshua	POPL '17: "Sums of Uncertainty: Refinements ..." Sums of Uncertainty: Refinements Go Gradual Khurram A. Jafery and Joshua Dunfield (University of British Columbia, Canada) @InProceedings{POPL17p1111, author = {Khurram A. Jafery and Joshua Dunfield}, title = {Sums of Uncertainty: Refinements Go Gradual}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1111-1110}, doi = {}, year = {2017}, } Article: popl17main-main142-p (type: Full Paper) doi:
	Enea, Constantin	POPL '17: "On Verifying Causal Consistency ..." On Verifying Causal Consistency Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza (University of Paris Diderot, France; EPFL, Switzerland; Inria, France) @InProceedings{POPL17p903, author = {Ahmed Bouajjani and Constantin Enea and Rachid Guerraoui and Jad Hamza}, title = {On Verifying Causal Consistency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {903-902}, doi = {}, year = {2017}, } Article: popl17main-main255-p (type: Full Paper) doi:
	Faggian, Claudia	POPL '17: "The Geometry of Parallelism: ..." The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu (University of Bologna, Italy; Inria, France; CNRS, France; University of Paris Diderot, France; University of Paris-Saclay, France; University of Tokyo, Japan) @InProceedings{POPL17p1143, author = {Ugo Dal Lago and Claudia Faggian and Benoît Valiron and Akira Yoshimizu}, title = {The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1143-1142}, doi = {}, year = {2017}, } Article: popl17main-main113-p (type: Full Paper) doi:
	Feng, Yu	POPL '17: "Component-Based Synthesis ..." Component-Based Synthesis for Complex APIs Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps (University of Texas at Austin, USA; University of Wisconsin-Madison, USA) @InProceedings{POPL17p871, author = {Yu Feng and Ruben Martins and Yuepeng Wang and Isil Dillig and Thomas W. Reps}, title = {Component-Based Synthesis for Complex APIs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {871-870}, doi = {}, year = {2017}, } Article: popl17main-main93-p (type: Full Paper) doi:
	Flur, Shaked	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Foster, Nate	POPL '17: "Cantor Meets Scott: Semantic ..." Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University College London, UK) @InProceedings{POPL17p823, author = {Steffen Smolka and Praveen Kumar and Nate Foster and Dexter Kozen and Alexandra Silva}, title = {Cantor Meets Scott: Semantic Foundations for Probabilistic Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {823-822}, doi = {}, year = {2017}, } Article: popl17main-main18-p (type: Full Paper) doi:
	Gaboardi, Marco	POPL '17: "Relational Cost Analysis ..." Relational Cost Analysis Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann (MPI-SWS, Germany; IMDEA Software Institute, Spain; SUNY Buffalo, USA; Carnegie Mellon University, USA) @InProceedings{POPL17p551, author = {Ezgi Çiçek and Gilles Barthe and Marco Gaboardi and Deepak Garg and Jan Hoffmann}, title = {Relational Cost Analysis}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {551-550}, doi = {}, year = {2017}, } Article: popl17main-main107-p (type: Full Paper) doi: POPL '17: "A Semantic Account of Metric ..." A Semantic Account of Metric Preservation Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui (University of Pennsylvania, USA; SUNY Buffalo, USA; Kyoto University, Japan; ENS, France) @InProceedings{POPL17p807, author = {Arthur Azevedo de Amorim and Marco Gaboardi and Justin Hsu and Shin-ya Katsumata and Ikram Cherigui}, title = {A Semantic Account of Metric Preservation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {807-806}, doi = {}, year = {2017}, } Article: popl17main-main259-p (type: Full Paper) doi:
	Gallois-Wong, Diane	POPL '17: "Beginner's Luck: A Language ..." Beginner's Luck: A Language for Property-Based Generators Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia (University of Pennsylvania, USA; Inria, France; ENS, France; Chalmers University of Technology, Sweden) @InProceedings{POPL17p327, author = {Leonidas Lampropoulos and Diane Gallois-Wong and Cătălin Hriţcu and John Hughes and Benjamin C. Pierce and Li-yao Xia}, title = {Beginner's Luck: A Language for Property-Based Generators}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {327-326}, doi = {}, year = {2017}, } Article: popl17main-main152-p (type: Full Paper) doi:
	Garg, Deepak	POPL '17: "Relational Cost Analysis ..." Relational Cost Analysis Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann (MPI-SWS, Germany; IMDEA Software Institute, Spain; SUNY Buffalo, USA; Carnegie Mellon University, USA) @InProceedings{POPL17p551, author = {Ezgi Çiçek and Gilles Barthe and Marco Gaboardi and Deepak Garg and Jan Hoffmann}, title = {Relational Cost Analysis}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {551-550}, doi = {}, year = {2017}, } Article: popl17main-main107-p (type: Full Paper) doi:
	Germane, Kimball	POPL '17: "A Posteriori Environment Analysis ..." A Posteriori Environment Analysis with Pushdown Delta CFA Kimball Germane and Matthew Might (University of Utah, USA) @InProceedings{POPL17p215, author = {Kimball Germane and Matthew Might}, title = {A Posteriori Environment Analysis with Pushdown Delta CFA}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {215-214}, doi = {}, year = {2017}, } Article: popl17main-main312-p (type: Full Paper) doi:
	Gopalakrishnan, Ganesh	POPL '17: "Rigorous Floating-Point Mixed-Precision ..." Rigorous Floating-Point Mixed-Precision Tuning Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić (University of Utah, USA) @InProceedings{POPL17p535, author = {Wei-Fan Chiang and Mark Baranowski and Ian Briggs and Alexey Solovyev and Ganesh Gopalakrishnan and Zvonimir Rakamarić}, title = {Rigorous Floating-Point Mixed-Precision Tuning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {535-534}, doi = {}, year = {2017}, } Article: popl17main-main41-p (type: Full Paper) doi:
	Gray, Kathryn E.	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Greenman, Ben	POPL '17: "Type Systems as Macros ..." Type Systems as Macros Stephen Chang, Alex Knauth, and Ben Greenman (Northeastern University, USA) @InProceedings{POPL17p983, author = {Stephen Chang and Alex Knauth and Ben Greenman}, title = {Type Systems as Macros}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {983-982}, doi = {}, year = {2017}, } Article: popl17main-main247-p (type: Full Paper) doi:
	Grégoire, Benjamin	POPL '17: "Coupling Proofs Are Probabilistic ..." Coupling Proofs Are Probabilistic Product Programs Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; Inria, France; University of Pennsylvania, USA; École Polytechnique, France) @InProceedings{POPL17p375, author = {Gilles Barthe and Benjamin Grégoire and Justin Hsu and Pierre-Yves Strub}, title = {Coupling Proofs Are Probabilistic Product Programs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {375-374}, doi = {}, year = {2017}, } Article: popl17main-main290-p (type: Full Paper) doi:
	Grigore, Radu	POPL '17: "Java Generics Are Turing Complete ..." Java Generics Are Turing Complete Radu Grigore (University of Kent, UK) @InProceedings{POPL17p279, author = {Radu Grigore}, title = {Java Generics Are Turing Complete}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {279-278}, doi = {}, year = {2017}, } Article: popl17main-main163-p (type: Full Paper) doi:
	Guerraoui, Rachid	POPL '17: "On Verifying Causal Consistency ..." On Verifying Causal Consistency Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza (University of Paris Diderot, France; EPFL, Switzerland; Inria, France) @InProceedings{POPL17p903, author = {Ahmed Bouajjani and Constantin Enea and Rachid Guerraoui and Jad Hamza}, title = {On Verifying Causal Consistency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {903-902}, doi = {}, year = {2017}, } Article: popl17main-main255-p (type: Full Paper) doi:
	Hammer, Matthew A.	POPL '17: "Hazelnut: A Bidirectionally ..." Hazelnut: A Bidirectionally Typed Structure Editor Calculus Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer (Carnegie Mellon University, USA; Oregon State University, USA; University of Colorado at Boulder, USA) @InProceedings{POPL17p295, author = {Cyrus Omar and Ian Voysey and Michael Hilton and Jonathan Aldrich and Matthew A. Hammer}, title = {Hazelnut: A Bidirectionally Typed Structure Editor Calculus}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {295-294}, doi = {}, year = {2017}, } Article: popl17main-main319-p (type: Full Paper) doi:
	Hamza, Jad	POPL '17: "On Verifying Causal Consistency ..." On Verifying Causal Consistency Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza (University of Paris Diderot, France; EPFL, Switzerland; Inria, France) @InProceedings{POPL17p903, author = {Ahmed Bouajjani and Constantin Enea and Rachid Guerraoui and Jad Hamza}, title = {On Verifying Causal Consistency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {903-902}, doi = {}, year = {2017}, } Article: popl17main-main255-p (type: Full Paper) doi:
	Harper, Robert	POPL '17: "Computational Higher-Dimensional ..." Computational Higher-Dimensional Type Theory Carlo Angiuli, Robert Harper, and Todd Wilson (Carnegie Mellon University, USA; California State University at Fresno, USA) @InProceedings{POPL17p967, author = {Carlo Angiuli and Robert Harper and Todd Wilson}, title = {Computational Higher-Dimensional Type Theory}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {967-966}, doi = {}, year = {2017}, } Article: popl17main-main126-p (type: Full Paper) doi: POPL '17: "Parallel Functional Arrays ..." Parallel Functional Arrays Ananya Kumar, Guy E. Blelloch, and Robert Harper (Carnegie Mellon University, USA) @InProceedings{POPL17p999, author = {Ananya Kumar and Guy E. Blelloch and Robert Harper}, title = {Parallel Functional Arrays}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {999-998}, doi = {}, year = {2017}, } Article: popl17main-main157-p (type: Full Paper) doi:
	Harris, William R.	POPL '17: "Complexity Verification using ..." Complexity Verification using Guided Theorem Enumeration Akhilesh Srikanth, Burak Sahin, and William R. Harris (Georgia Institute of Technology, USA) @InProceedings{POPL17p919, author = {Akhilesh Srikanth and Burak Sahin and William R. Harris}, title = {Complexity Verification using Guided Theorem Enumeration}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {919-918}, doi = {}, year = {2017}, } Article: popl17main-main137-p (type: Full Paper) doi:
	Hilton, Michael	POPL '17: "Hazelnut: A Bidirectionally ..." Hazelnut: A Bidirectionally Typed Structure Editor Calculus Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer (Carnegie Mellon University, USA; Oregon State University, USA; University of Colorado at Boulder, USA) @InProceedings{POPL17p295, author = {Cyrus Omar and Ian Voysey and Michael Hilton and Jonathan Aldrich and Matthew A. Hammer}, title = {Hazelnut: A Bidirectionally Typed Structure Editor Calculus}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {295-294}, doi = {}, year = {2017}, } Article: popl17main-main319-p (type: Full Paper) doi:
	Hoenicke, Jochen	POPL '17: "Thread Modularity at Many ..." Thread Modularity at Many Levels: A Pearl in Compositional Verification Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski (University of Freiburg, Germany; MPI-SWS, Germany) @InProceedings{POPL17p727, author = {Jochen Hoenicke and Rupak Majumdar and Andreas Podelski}, title = {Thread Modularity at Many Levels: A Pearl in Compositional Verification}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {727-726}, doi = {}, year = {2017}, } Article: popl17main-main273-p (type: Full Paper) doi:
	Hoffmann, Jan	POPL '17: "Relational Cost Analysis ..." Relational Cost Analysis Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann (MPI-SWS, Germany; IMDEA Software Institute, Spain; SUNY Buffalo, USA; Carnegie Mellon University, USA) @InProceedings{POPL17p551, author = {Ezgi Çiçek and Gilles Barthe and Marco Gaboardi and Deepak Garg and Jan Hoffmann}, title = {Relational Cost Analysis}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {551-550}, doi = {}, year = {2017}, } Article: popl17main-main107-p (type: Full Paper) doi: POPL '17: "Towards Automatic Resource ..." Towards Automatic Resource Bound Analysis for OCaml Jan Hoffmann, Ankush Das, and Shu-Chun Weng (Carnegie Mellon University, USA; Yale University, USA) @InProceedings{POPL17p599, author = {Jan Hoffmann and Ankush Das and Shu-Chun Weng}, title = {Towards Automatic Resource Bound Analysis for OCaml}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {599-598}, doi = {}, year = {2017}, } Article: popl17main-main17-p (type: Full Paper) doi:
	Hriţcu, Cătălin	POPL '17: "Beginner's Luck: A Language ..." Beginner's Luck: A Language for Property-Based Generators Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia (University of Pennsylvania, USA; Inria, France; ENS, France; Chalmers University of Technology, Sweden) @InProceedings{POPL17p327, author = {Leonidas Lampropoulos and Diane Gallois-Wong and Cătălin Hriţcu and John Hughes and Benjamin C. Pierce and Li-yao Xia}, title = {Beginner's Luck: A Language for Property-Based Generators}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {327-326}, doi = {}, year = {2017}, } Article: popl17main-main152-p (type: Full Paper) doi: POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Hsu, Justin	POPL '17: "Coupling Proofs Are Probabilistic ..." Coupling Proofs Are Probabilistic Product Programs Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; Inria, France; University of Pennsylvania, USA; École Polytechnique, France) @InProceedings{POPL17p375, author = {Gilles Barthe and Benjamin Grégoire and Justin Hsu and Pierre-Yves Strub}, title = {Coupling Proofs Are Probabilistic Product Programs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {375-374}, doi = {}, year = {2017}, } Article: popl17main-main290-p (type: Full Paper) doi: POPL '17: "A Semantic Account of Metric ..." A Semantic Account of Metric Preservation Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui (University of Pennsylvania, USA; SUNY Buffalo, USA; Kyoto University, Japan; ENS, France) @InProceedings{POPL17p807, author = {Arthur Azevedo de Amorim and Marco Gaboardi and Justin Hsu and Shin-ya Katsumata and Ikram Cherigui}, title = {A Semantic Account of Metric Preservation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {807-806}, doi = {}, year = {2017}, } Article: popl17main-main259-p (type: Full Paper) doi:
	Hughes, John	POPL '17: "Beginner's Luck: A Language ..." Beginner's Luck: A Language for Property-Based Generators Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia (University of Pennsylvania, USA; Inria, France; ENS, France; Chalmers University of Technology, Sweden) @InProceedings{POPL17p327, author = {Leonidas Lampropoulos and Diane Gallois-Wong and Cătălin Hriţcu and John Hughes and Benjamin C. Pierce and Li-yao Xia}, title = {Beginner's Luck: A Language for Property-Based Generators}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {327-326}, doi = {}, year = {2017}, } Article: popl17main-main152-p (type: Full Paper) doi:
	Hur, Chung-Kil	POPL '17: "A Promising Semantics for ..." A Promising Semantics for Relaxed-Memory Concurrency Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) @InProceedings{POPL17p391, author = {Jeehoon Kang and Chung-Kil Hur and Ori Lahav and Viktor Vafeiadis and Derek Dreyer}, title = {A Promising Semantics for Relaxed-Memory Concurrency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {391-390}, doi = {}, year = {2017}, } Article: popl17main-main65-p (type: Full Paper) doi:
	Igarashi, Atsushi	POPL '17: "Stateful Manifest Contracts ..." Stateful Manifest Contracts Taro Sekiyama and Atsushi Igarashi (IBM Research, Japan; Kyoto University, Japan) @InProceedings{POPL17p791, author = {Taro Sekiyama and Atsushi Igarashi}, title = {Stateful Manifest Contracts}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {791-790}, doi = {}, year = {2017}, } Article: popl17main-main187-p (type: Full Paper) doi:
	Ilik, Danko	POPL '17: "The exp-log Normal Form of ..." The exp-log Normal Form of Types: Decomposing Extensional Equality and Representing Terms Compactly Danko Ilik (Trusted Labs, France) @InProceedings{POPL17p631, author = {Danko Ilik}, title = {The exp-log Normal Form of Types: Decomposing Extensional Equality and Representing Terms Compactly}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {631-630}, doi = {}, year = {2017}, } Article: popl17main-main11-p (type: Full Paper) doi:
	Jafery, Khurram A.	POPL '17: "Sums of Uncertainty: Refinements ..." Sums of Uncertainty: Refinements Go Gradual Khurram A. Jafery and Joshua Dunfield (University of British Columbia, Canada) @InProceedings{POPL17p1111, author = {Khurram A. Jafery and Joshua Dunfield}, title = {Sums of Uncertainty: Refinements Go Gradual}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1111-1110}, doi = {}, year = {2017}, } Article: popl17main-main142-p (type: Full Paper) doi:
	Kang, Jeehoon	POPL '17: "A Promising Semantics for ..." A Promising Semantics for Relaxed-Memory Concurrency Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) @InProceedings{POPL17p391, author = {Jeehoon Kang and Chung-Kil Hur and Ori Lahav and Viktor Vafeiadis and Derek Dreyer}, title = {A Promising Semantics for Relaxed-Memory Concurrency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {391-390}, doi = {}, year = {2017}, } Article: popl17main-main65-p (type: Full Paper) doi:
	Katsumata, Shin-ya	POPL '17: "A Semantic Account of Metric ..." A Semantic Account of Metric Preservation Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui (University of Pennsylvania, USA; SUNY Buffalo, USA; Kyoto University, Japan; ENS, France) @InProceedings{POPL17p807, author = {Arthur Azevedo de Amorim and Marco Gaboardi and Justin Hsu and Shin-ya Katsumata and Ikram Cherigui}, title = {A Semantic Account of Metric Preservation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {807-806}, doi = {}, year = {2017}, } Article: popl17main-main259-p (type: Full Paper) doi:
	Kifer, Daniel	POPL '17: "LightDP: Towards Automating ..." LightDP: Towards Automating Differential Privacy Proofs Danfeng Zhang and Daniel Kifer (Pennsylvania State University, USA) @InProceedings{POPL17p1207, author = {Danfeng Zhang and Daniel Kifer}, title = {LightDP: Towards Automating Differential Privacy Proofs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1207-1206}, doi = {}, year = {2017}, } Article: popl17main-main234-p (type: Full Paper) doi:
	Kiselyov, Oleg	POPL '17: "Stream Fusion, to Completeness ..." Stream Fusion, to Completeness Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, and Yannis Smaragdakis (Tohoku University, Japan; University of Athens, Greece; Nessos IT, Greece) @InProceedings{POPL17p519, author = {Oleg Kiselyov and Aggelos Biboudis and Nick Palladinos and Yannis Smaragdakis}, title = {Stream Fusion, to Completeness}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {519-518}, doi = {}, year = {2017}, } Article: popl17main-main218-p (type: Full Paper) doi:
	Klin, Bartek	POPL '17: "Learning Nominal Automata ..." Learning Nominal Automata Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michał Szynwelski (Radboud University Nijmegen, Netherlands; University College London, UK; University of Warsaw, Poland) @InProceedings{POPL17p887, author = {Joshua Moerman and Matteo Sammartino and Alexandra Silva and Bartek Klin and Michał Szynwelski}, title = {Learning Nominal Automata}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {887-886}, doi = {}, year = {2017}, } Article: popl17main-main209-p (type: Full Paper) doi:
	Knauth, Alex	POPL '17: "Type Systems as Macros ..." Type Systems as Macros Stephen Chang, Alex Knauth, and Ben Greenman (Northeastern University, USA) @InProceedings{POPL17p983, author = {Stephen Chang and Alex Knauth and Ben Greenman}, title = {Type Systems as Macros}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {983-982}, doi = {}, year = {2017}, } Article: popl17main-main247-p (type: Full Paper) doi:
	Kobayashi, Naoki	POPL '17: "On the Relationship between ..." On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic Naoki Kobayashi, Étienne Lozes, and Florian Bruse (University of Tokyo, Japan; ENS, France; CNRS, France; University of Kassel, Germany) @InProceedings{POPL17p471, author = {Naoki Kobayashi and Étienne Lozes and Florian Bruse}, title = {On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {471-470}, doi = {}, year = {2017}, } Article: popl17main-main97-p (type: Full Paper) doi:
	Konnov, Igor	POPL '17: "A Short Counterexample Property ..." A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder (Vienna University of Technology, Austria) @InProceedings{POPL17p1015, author = {Igor Konnov and Marijana Lazić and Helmut Veith and Josef Widder}, title = {A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1015-1014}, doi = {}, year = {2017}, } Article: popl17main-main116-p (type: Full Paper) doi:
	Kopczyński, Eryk	POPL '17: "LOIS: Syntax and Semantics ..." LOIS: Syntax and Semantics Eryk Kopczyński and Szymon Toruńczyk (University of Warsaw, Poland) @InProceedings{POPL17p855, author = {Eryk Kopczyński and Szymon Toruńczyk}, title = {LOIS: Syntax and Semantics}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {855-854}, doi = {}, year = {2017}, } Article: popl17main-main189-p (type: Full Paper) doi:
	Kovács, Laura	POPL '17: "Coming to Terms with Quantified ..." Coming to Terms with Quantified Reasoning Laura Kovács, Simon Robillard, and Andrei Voronkov (Vienna University of Technology, Austria; Chalmers University of Technology, Sweden; University of Manchester, UK) @InProceedings{POPL17p487, author = {Laura Kovács and Simon Robillard and Andrei Voronkov}, title = {Coming to Terms with Quantified Reasoning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {487-486}, doi = {}, year = {2017}, } Article: popl17main-main253-p (type: Full Paper) doi:
	Kozen, Dexter	POPL '17: "Cantor Meets Scott: Semantic ..." Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University College London, UK) @InProceedings{POPL17p823, author = {Steffen Smolka and Praveen Kumar and Nate Foster and Dexter Kozen and Alexandra Silva}, title = {Cantor Meets Scott: Semantic Foundations for Probabilistic Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {823-822}, doi = {}, year = {2017}, } Article: popl17main-main18-p (type: Full Paper) doi:
	Krebbers, Robbert	POPL '17: "Interactive Proofs in Higher-Order ..." Interactive Proofs in Higher-Order Concurrent Separation Logic Robbert Krebbers, Amin Timany, and Lars Birkedal (Delft University of Technology, Netherlands; KU Leuven, Belgium; Aarhus University, Denmark) @InProceedings{POPL17p423, author = {Robbert Krebbers and Amin Timany and Lars Birkedal}, title = {Interactive Proofs in Higher-Order Concurrent Separation Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, } Article: popl17main-main99-p (type: Full Paper) doi:
	Krogh-Jespersen, Morten	POPL '17: "A Relational Model of Types-and-Effects ..." A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal (Aarhus University, Denmark; University of Cambridge, UK) @InProceedings{POPL17p439, author = {Morten Krogh-Jespersen and Kasper Svendsen and Lars Birkedal}, title = {A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {439-438}, doi = {}, year = {2017}, } Article: popl17main-main192-p (type: Full Paper) doi:
	Kulal, Sumith	POPL '17: "Contract-Based Resource Verification ..." Contract-Based Resource Verification for Higher-Order Functions with Memoization Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak (EPFL, Switzerland; IIT Bombay, India) @InProceedings{POPL17p567, author = {Ravichandhran Madhavan and Sumith Kulal and Viktor Kuncak}, title = {Contract-Based Resource Verification for Higher-Order Functions with Memoization}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {567-566}, doi = {}, year = {2017}, } Article: popl17main-main184-p (type: Full Paper) doi:
	Kumar, Ananya	POPL '17: "Parallel Functional Arrays ..." Parallel Functional Arrays Ananya Kumar, Guy E. Blelloch, and Robert Harper (Carnegie Mellon University, USA) @InProceedings{POPL17p999, author = {Ananya Kumar and Guy E. Blelloch and Robert Harper}, title = {Parallel Functional Arrays}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {999-998}, doi = {}, year = {2017}, } Article: popl17main-main157-p (type: Full Paper) doi:
	Kumar, Praveen	POPL '17: "Cantor Meets Scott: Semantic ..." Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University College London, UK) @InProceedings{POPL17p823, author = {Steffen Smolka and Praveen Kumar and Nate Foster and Dexter Kozen and Alexandra Silva}, title = {Cantor Meets Scott: Semantic Foundations for Probabilistic Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {823-822}, doi = {}, year = {2017}, } Article: popl17main-main18-p (type: Full Paper) doi:
	Kuncak, Viktor	POPL '17: "Contract-Based Resource Verification ..." Contract-Based Resource Verification for Higher-Order Functions with Memoization Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak (EPFL, Switzerland; IIT Bombay, India) @InProceedings{POPL17p567, author = {Ravichandhran Madhavan and Sumith Kulal and Viktor Kuncak}, title = {Contract-Based Resource Verification for Higher-Order Functions with Memoization}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {567-566}, doi = {}, year = {2017}, } Article: popl17main-main184-p (type: Full Paper) doi:
	Lahav, Ori	POPL '17: "A Promising Semantics for ..." A Promising Semantics for Relaxed-Memory Concurrency Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) @InProceedings{POPL17p391, author = {Jeehoon Kang and Chung-Kil Hur and Ori Lahav and Viktor Vafeiadis and Derek Dreyer}, title = {A Promising Semantics for Relaxed-Memory Concurrency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {391-390}, doi = {}, year = {2017}, } Article: popl17main-main65-p (type: Full Paper) doi:
	Lampropoulos, Leonidas	POPL '17: "Beginner's Luck: A Language ..." Beginner's Luck: A Language for Property-Based Generators Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia (University of Pennsylvania, USA; Inria, France; ENS, France; Chalmers University of Technology, Sweden) @InProceedings{POPL17p327, author = {Leonidas Lampropoulos and Diane Gallois-Wong and Cătălin Hriţcu and John Hughes and Benjamin C. Pierce and Li-yao Xia}, title = {Beginner's Luck: A Language for Property-Based Generators}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {327-326}, doi = {}, year = {2017}, } Article: popl17main-main152-p (type: Full Paper) doi:
	Lange, Julien	POPL '17: "Fencing off Go: Liveness and ..." Fencing off Go: Liveness and Safety for Channel-Based Programming Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida (Imperial College London, UK) @InProceedings{POPL17p1047, author = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida}, title = {Fencing off Go: Liveness and Safety for Channel-Based Programming}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1047-1046}, doi = {}, year = {2017}, } Article: popl17main-main51-p (type: Full Paper) doi:
	Lazić, Marijana	POPL '17: "A Short Counterexample Property ..." A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder (Vienna University of Technology, Austria) @InProceedings{POPL17p1015, author = {Igor Konnov and Marijana Lazić and Helmut Veith and Josef Widder}, title = {A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1015-1014}, doi = {}, year = {2017}, } Article: popl17main-main116-p (type: Full Paper) doi:
	Lehmann, Nico	POPL '17: "Gradual Refinement Types ..." Gradual Refinement Types Nico Lehmann and Éric Tanter (University of Chile, Chile) @InProceedings{POPL17p1079, author = {Nico Lehmann and Éric Tanter}, title = {Gradual Refinement Types}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1079-1078}, doi = {}, year = {2017}, } Article: popl17main-main102-p (type: Full Paper) doi:
	Leijen, Daan	POPL '17: "Type Directed Compilation ..." Type Directed Compilation of Row-Typed Algebraic Effects Daan Leijen (Microsoft Research, USA) @InProceedings{POPL17p743, author = {Daan Leijen}, title = {Type Directed Compilation of Row-Typed Algebraic Effects}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {743-742}, doi = {}, year = {2017}, } Article: popl17main-main164-p (type: Full Paper) doi:
	Levy, Paul Blain	POPL '17: "Contextual Isomorphisms ..." Contextual Isomorphisms Paul Blain Levy (University of Birmingham, UK) @InProceedings{POPL17p647, author = {Paul Blain Levy}, title = {Contextual Isomorphisms}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {647-646}, doi = {}, year = {2017}, } Article: popl17main-main305-p (type: Full Paper) doi:
	Li, Huisong	POPL '17: "Semantic-Directed Clumping ..." Semantic-Directed Clumping of Disjunctive Abstract States Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival (Inria, France; CNRS, France; ENS, France; University of Colorado at Boulder, USA) @InProceedings{POPL17p231, author = {Huisong Li and Francois Berenger and Bor-Yuh Evan Chang and Xavier Rival}, title = {Semantic-Directed Clumping of Disjunctive Abstract States}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {231-230}, doi = {}, year = {2017}, } Article: popl17main-main220-p (type: Full Paper) doi:
	Lidbury, Christopher	POPL '17: "Dynamic Race Detection for ..." Dynamic Race Detection for C++11 Christopher Lidbury and Alastair F. Donaldson (Imperial College London, UK) @InProceedings{POPL17p695, author = {Christopher Lidbury and Alastair F. Donaldson}, title = {Dynamic Race Detection for C++11}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {695-694}, doi = {}, year = {2017}, } Article: popl17main-main106-p (type: Full Paper) doi:
	Lindley, Sam	POPL '17: "Do Be Do Be Do ..." Do Be Do Be Do Sam Lindley, Conor McBride, and Craig McLaughlin (University of Edinburgh, UK; University of Strathclyde, UK) @InProceedings{POPL17p759, author = {Sam Lindley and Conor McBride and Craig McLaughlin}, title = {Do Be Do Be Do}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {759-758}, doi = {}, year = {2017}, } Article: popl17main-main302-p (type: Full Paper) doi:
	Liu, Xinxin	POPL '17: "Analyzing Divergence in Bisimulation ..." Analyzing Divergence in Bisimulation Semantics Xinxin Liu, Tingting Yu, and Wenhui Zhang (Institute of Software at Chinese Academy of Sciences, China) @InProceedings{POPL17p1031, author = {Xinxin Liu and Tingting Yu and Wenhui Zhang}, title = {Analyzing Divergence in Bisimulation Semantics}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1031-1030}, doi = {}, year = {2017}, } Article: popl17main-main158-p (type: Full Paper) doi:
	Lozes, Étienne	POPL '17: "On the Relationship between ..." On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic Naoki Kobayashi, Étienne Lozes, and Florian Bruse (University of Tokyo, Japan; ENS, France; CNRS, France; University of Kassel, Germany) @InProceedings{POPL17p471, author = {Naoki Kobayashi and Étienne Lozes and Florian Bruse}, title = {On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {471-470}, doi = {}, year = {2017}, } Article: popl17main-main97-p (type: Full Paper) doi:
	Madhavan, Ravichandhran	POPL '17: "Contract-Based Resource Verification ..." Contract-Based Resource Verification for Higher-Order Functions with Memoization Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak (EPFL, Switzerland; IIT Bombay, India) @InProceedings{POPL17p567, author = {Ravichandhran Madhavan and Sumith Kulal and Viktor Kuncak}, title = {Contract-Based Resource Verification for Higher-Order Functions with Memoization}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {567-566}, doi = {}, year = {2017}, } Article: popl17main-main184-p (type: Full Paper) doi:
	Maillard, Kenji	POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Majumdar, Rupak	POPL '17: "Thread Modularity at Many ..." Thread Modularity at Many Levels: A Pearl in Compositional Verification Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski (University of Freiburg, Germany; MPI-SWS, Germany) @InProceedings{POPL17p727, author = {Jochen Hoenicke and Rupak Majumdar and Andreas Podelski}, title = {Thread Modularity at Many Levels: A Pearl in Compositional Verification}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {727-726}, doi = {}, year = {2017}, } Article: popl17main-main273-p (type: Full Paper) doi:
	Maranget, Luc	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Martínez, Guido	POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Martins, Ruben	POPL '17: "Component-Based Synthesis ..." Component-Based Synthesis for Complex APIs Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps (University of Texas at Austin, USA; University of Wisconsin-Madison, USA) @InProceedings{POPL17p871, author = {Yu Feng and Ruben Martins and Yuepeng Wang and Isil Dillig and Thomas W. Reps}, title = {Component-Based Synthesis for Complex APIs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {871-870}, doi = {}, year = {2017}, } Article: popl17main-main93-p (type: Full Paper) doi:
	McBride, Conor	POPL '17: "Do Be Do Be Do ..." Do Be Do Be Do Sam Lindley, Conor McBride, and Craig McLaughlin (University of Edinburgh, UK; University of Strathclyde, UK) @InProceedings{POPL17p759, author = {Sam Lindley and Conor McBride and Craig McLaughlin}, title = {Do Be Do Be Do}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {759-758}, doi = {}, year = {2017}, } Article: popl17main-main302-p (type: Full Paper) doi:
	McLaughlin, Craig	POPL '17: "Do Be Do Be Do ..." Do Be Do Be Do Sam Lindley, Conor McBride, and Craig McLaughlin (University of Edinburgh, UK; University of Strathclyde, UK) @InProceedings{POPL17p759, author = {Sam Lindley and Conor McBride and Craig McLaughlin}, title = {Do Be Do Be Do}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {759-758}, doi = {}, year = {2017}, } Article: popl17main-main302-p (type: Full Paper) doi:
	Might, Matthew	POPL '17: "A Posteriori Environment Analysis ..." A Posteriori Environment Analysis with Pushdown Delta CFA Kimball Germane and Matthew Might (University of Utah, USA) @InProceedings{POPL17p215, author = {Kimball Germane and Matthew Might}, title = {A Posteriori Environment Analysis with Pushdown Delta CFA}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {215-214}, doi = {}, year = {2017}, } Article: popl17main-main312-p (type: Full Paper) doi:
	Moerman, Joshua	POPL '17: "Learning Nominal Automata ..." Learning Nominal Automata Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michał Szynwelski (Radboud University Nijmegen, Netherlands; University College London, UK; University of Warsaw, Poland) @InProceedings{POPL17p887, author = {Joshua Moerman and Matteo Sammartino and Alexandra Silva and Bartek Klin and Michał Szynwelski}, title = {Learning Nominal Automata}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {887-886}, doi = {}, year = {2017}, } Article: popl17main-main209-p (type: Full Paper) doi:
	Müller, Peter	POPL '17: "Serializability for Eventual ..." Serializability for Eventual Consistency: Criterion, Analysis, and Applications Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev (ETH Zurich, Switzerland) @InProceedings{POPL17p711, author = {Lucas Brutschy and Dimitar Dimitrov and Peter Müller and Martin Vechev}, title = {Serializability for Eventual Consistency: Criterion, Analysis, and Applications}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {711-710}, doi = {}, year = {2017}, } Article: popl17main-main285-p (type: Full Paper) doi:
	Mycroft, Alan	POPL '17: "Polymorphism, Subtyping, and ..." Polymorphism, Subtyping, and Type Inference in MLsub Stephen Dolan and Alan Mycroft (University of Cambridge, UK) @InProceedings{POPL17p263, author = {Stephen Dolan and Alan Mycroft}, title = {Polymorphism, Subtyping, and Type Inference in MLsub}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {263-262}, doi = {}, year = {2017}, } Article: popl17main-main228-p (type: Full Paper) doi:
	Naumann, David A.	POPL '17: "Hypercollecting Semantics ..." Hypercollecting Semantics and Its Application to Static Analysis of Information Flow Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel (Stevens Institute of Technology, USA; CEA LIST, France; CentraleSupélec, France) @InProceedings{POPL17p1191, author = {Mounir Assaf and David A. Naumann and Julien Signoles and Éric Totel and Frédéric Tronel}, title = {Hypercollecting Semantics and Its Application to Static Analysis of Information Flow}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1191-1190}, doi = {}, year = {2017}, } Article: popl17main-main256-p (type: Full Paper) doi:
	Ng, Nicholas	POPL '17: "Fencing off Go: Liveness and ..." Fencing off Go: Liveness and Safety for Channel-Based Programming Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida (Imperial College London, UK) @InProceedings{POPL17p1047, author = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida}, title = {Fencing off Go: Liveness and Safety for Channel-Based Programming}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1047-1046}, doi = {}, year = {2017}, } Article: popl17main-main51-p (type: Full Paper) doi:
	Nienhuis, Kyndylan	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Novotný, Petr	POPL '17: "Stochastic Invariants for ..." Stochastic Invariants for Probabilistic Termination Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić (IST Austria, Austria; University of Cambridge, UK) @InProceedings{POPL17p359, author = {Krishnendu Chatterjee and Petr Novotný and Ðorđe Žikelić}, title = {Stochastic Invariants for Probabilistic Termination}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {359-358}, doi = {}, year = {2017}, } Article: popl17main-main182-p (type: Full Paper) doi:
	Omar, Cyrus	POPL '17: "Hazelnut: A Bidirectionally ..." Hazelnut: A Bidirectionally Typed Structure Editor Calculus Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer (Carnegie Mellon University, USA; Oregon State University, USA; University of Colorado at Boulder, USA) @InProceedings{POPL17p295, author = {Cyrus Omar and Ian Voysey and Michael Hilton and Jonathan Aldrich and Matthew A. Hammer}, title = {Hazelnut: A Bidirectionally Typed Structure Editor Calculus}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {295-294}, doi = {}, year = {2017}, } Article: popl17main-main319-p (type: Full Paper) doi:
	Palladinos, Nick	POPL '17: "Stream Fusion, to Completeness ..." Stream Fusion, to Completeness Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, and Yannis Smaragdakis (Tohoku University, Japan; University of Athens, Greece; Nessos IT, Greece) @InProceedings{POPL17p519, author = {Oleg Kiselyov and Aggelos Biboudis and Nick Palladinos and Yannis Smaragdakis}, title = {Stream Fusion, to Completeness}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {519-518}, doi = {}, year = {2017}, } Article: popl17main-main218-p (type: Full Paper) doi:
	Palsberg, Jens	POPL '17: "Typed Self-Evaluation via ..." Typed Self-Evaluation via Intensional Type Functions Matt Brown and Jens Palsberg (University of California at Los Angeles, USA) @InProceedings{POPL17p663, author = {Matt Brown and Jens Palsberg}, title = {Typed Self-Evaluation via Intensional Type Functions}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {663-662}, doi = {}, year = {2017}, } Article: popl17main-main96-p (type: Full Paper) doi:
	Paykin, Jennifer	POPL '17: "QWIRE: A Core Language for ..." QWIRE: A Core Language for Quantum Circuits Jennifer Paykin, Robert Rand, and Steve Zdancewic (University of Pennsylvania, USA) @InProceedings{POPL17p1159, author = {Jennifer Paykin and Robert Rand and Steve Zdancewic}, title = {QWIRE: A Core Language for Quantum Circuits}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1159-1158}, doi = {}, year = {2017}, } Article: popl17main-main278-p (type: Full Paper) doi:
	Pierce, Benjamin C.	POPL '17: "Beginner's Luck: A Language ..." Beginner's Luck: A Language for Property-Based Generators Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia (University of Pennsylvania, USA; Inria, France; ENS, France; Chalmers University of Technology, Sweden) @InProceedings{POPL17p327, author = {Leonidas Lampropoulos and Diane Gallois-Wong and Cătălin Hriţcu and John Hughes and Benjamin C. Pierce and Li-yao Xia}, title = {Beginner's Luck: A Language for Property-Based Generators}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {327-326}, doi = {}, year = {2017}, } Article: popl17main-main152-p (type: Full Paper) doi:
	Plotkin, Gordon	POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Podelski, Andreas	POPL '17: "Thread Modularity at Many ..." Thread Modularity at Many Levels: A Pearl in Compositional Verification Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski (University of Freiburg, Germany; MPI-SWS, Germany) @InProceedings{POPL17p727, author = {Jochen Hoenicke and Rupak Majumdar and Andreas Podelski}, title = {Thread Modularity at Many Levels: A Pearl in Compositional Verification}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {727-726}, doi = {}, year = {2017}, } Article: popl17main-main273-p (type: Full Paper) doi:
	Protzenko, Jonathan	POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Pulte, Christopher	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Püschel, Markus	POPL '17: "Fast Polyhedra Abstract Domain ..." Fast Polyhedra Abstract Domain Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) @InProceedings{POPL17p247, author = {Gagandeep Singh and Markus Püschel and Martin Vechev}, title = {Fast Polyhedra Abstract Domain}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {247-246}, doi = {}, year = {2017}, } Article: popl17main-main238-p (type: Full Paper) doi:
	Rakamarić, Zvonimir	POPL '17: "Rigorous Floating-Point Mixed-Precision ..." Rigorous Floating-Point Mixed-Precision Tuning Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić (University of Utah, USA) @InProceedings{POPL17p535, author = {Wei-Fan Chiang and Mark Baranowski and Ian Briggs and Alexey Solovyev and Ganesh Gopalakrishnan and Zvonimir Rakamarić}, title = {Rigorous Floating-Point Mixed-Precision Tuning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {535-534}, doi = {}, year = {2017}, } Article: popl17main-main41-p (type: Full Paper) doi:
	Ramsey, Norman	POPL '17: "Exact Bayesian Inference by ..." Exact Bayesian Inference by Symbolic Disintegration Chung-chieh Shan and Norman Ramsey (Indiana University, USA; Tufts University, USA) @InProceedings{POPL17p343, author = {Chung-chieh Shan and Norman Ramsey}, title = {Exact Bayesian Inference by Symbolic Disintegration}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {343-342}, doi = {}, year = {2017}, } Article: popl17main-main95-p (type: Full Paper) doi:
	Rand, Robert	POPL '17: "QWIRE: A Core Language for ..." QWIRE: A Core Language for Quantum Circuits Jennifer Paykin, Robert Rand, and Steve Zdancewic (University of Pennsylvania, USA) @InProceedings{POPL17p1159, author = {Jennifer Paykin and Robert Rand and Steve Zdancewic}, title = {QWIRE: A Core Language for Quantum Circuits}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1159-1158}, doi = {}, year = {2017}, } Article: popl17main-main278-p (type: Full Paper) doi:
	Rastogi, Aseem	POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Rehof, Jakob	POPL '17: "Intersection Type Calculi ..." Intersection Type Calculi of Bounded Dimension Andrej Dudenhefner and Jakob Rehof (TU Dortmund, Germany) @InProceedings{POPL17p935, author = {Andrej Dudenhefner and Jakob Rehof}, title = {Intersection Type Calculi of Bounded Dimension}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {935-934}, doi = {}, year = {2017}, } Article: popl17main-main130-p (type: Full Paper) doi:
	Reps, Thomas W.	POPL '17: "Component-Based Synthesis ..." Component-Based Synthesis for Complex APIs Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps (University of Texas at Austin, USA; University of Wisconsin-Madison, USA) @InProceedings{POPL17p871, author = {Yu Feng and Ruben Martins and Yuepeng Wang and Isil Dillig and Thomas W. Reps}, title = {Component-Based Synthesis for Complex APIs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {871-870}, doi = {}, year = {2017}, } Article: popl17main-main93-p (type: Full Paper) doi:
	Rival, Xavier	POPL '17: "Semantic-Directed Clumping ..." Semantic-Directed Clumping of Disjunctive Abstract States Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival (Inria, France; CNRS, France; ENS, France; University of Colorado at Boulder, USA) @InProceedings{POPL17p231, author = {Huisong Li and Francois Berenger and Bor-Yuh Evan Chang and Xavier Rival}, title = {Semantic-Directed Clumping of Disjunctive Abstract States}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {231-230}, doi = {}, year = {2017}, } Article: popl17main-main220-p (type: Full Paper) doi:
	Robillard, Simon	POPL '17: "Coming to Terms with Quantified ..." Coming to Terms with Quantified Reasoning Laura Kovács, Simon Robillard, and Andrei Voronkov (Vienna University of Technology, Austria; Chalmers University of Technology, Sweden; University of Manchester, UK) @InProceedings{POPL17p487, author = {Laura Kovács and Simon Robillard and Andrei Voronkov}, title = {Coming to Terms with Quantified Reasoning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {487-486}, doi = {}, year = {2017}, } Article: popl17main-main253-p (type: Full Paper) doi:
	Rompf, Tiark	POPL '17: "LMS-Verify: Abstraction without ..." LMS-Verify: Abstraction without Regret for Verified Systems Programming Nada Amin and Tiark Rompf (EPFL, Switzerland; Purdue University, USA) @InProceedings{POPL17p1175, author = {Nada Amin and Tiark Rompf}, title = {LMS-Verify: Abstraction without Regret for Verified Systems Programming}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1175-1174}, doi = {}, year = {2017}, } Article: popl17main-main144-p (type: Full Paper) doi: POPL '17: "Type Soundness Proofs with ..." Type Soundness Proofs with Definitional Interpreters Nada Amin and Tiark Rompf (EPFL, Switzerland; Purdue University, USA) @InProceedings{POPL17p951, author = {Nada Amin and Tiark Rompf}, title = {Type Soundness Proofs with Definitional Interpreters}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {951-950}, doi = {}, year = {2017}, } Article: popl17main-main143-p (type: Full Paper) doi:
	Sahin, Burak	POPL '17: "Complexity Verification using ..." Complexity Verification using Guided Theorem Enumeration Akhilesh Srikanth, Burak Sahin, and William R. Harris (Georgia Institute of Technology, USA) @InProceedings{POPL17p919, author = {Akhilesh Srikanth and Burak Sahin and William R. Harris}, title = {Complexity Verification using Guided Theorem Enumeration}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {919-918}, doi = {}, year = {2017}, } Article: popl17main-main137-p (type: Full Paper) doi:
	Sammartino, Matteo	POPL '17: "Learning Nominal Automata ..." Learning Nominal Automata Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michał Szynwelski (Radboud University Nijmegen, Netherlands; University College London, UK; University of Warsaw, Poland) @InProceedings{POPL17p887, author = {Joshua Moerman and Matteo Sammartino and Alexandra Silva and Bartek Klin and Michał Szynwelski}, title = {Learning Nominal Automata}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {887-886}, doi = {}, year = {2017}, } Article: popl17main-main209-p (type: Full Paper) doi:
	Sarkar, Susmit	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Scherer, Gabriel	POPL '17: "Deciding Equivalence with ..." Deciding Equivalence with Sums and the Empty Type Gabriel Scherer (Northeastern University, USA) @InProceedings{POPL17p615, author = {Gabriel Scherer}, title = {Deciding Equivalence with Sums and the Empty Type}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {615-614}, doi = {}, year = {2017}, } Article: popl17main-main355-p (type: Full Paper) doi:
	Scully, Ziv	POPL '17: "A Program Optimization for ..." A Program Optimization for Automatic Database Result Caching Ziv Scully and Adam Chlipala (Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA) @InProceedings{POPL17p503, author = {Ziv Scully and Adam Chlipala}, title = {A Program Optimization for Automatic Database Result Caching}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {503-502}, doi = {}, year = {2017}, } Article: popl17main-main260-p (type: Full Paper) doi:
	Sekiyama, Taro	POPL '17: "Stateful Manifest Contracts ..." Stateful Manifest Contracts Taro Sekiyama and Atsushi Igarashi (IBM Research, Japan; Kyoto University, Japan) @InProceedings{POPL17p791, author = {Taro Sekiyama and Atsushi Igarashi}, title = {Stateful Manifest Contracts}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {791-790}, doi = {}, year = {2017}, } Article: popl17main-main187-p (type: Full Paper) doi:
	Sewell, Peter	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Sezgin, Ali	POPL '17: "Mixed-Size Concurrency: ARM, ..." Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell (University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK) @InProceedings{POPL17p679, author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell}, title = {Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {679-678}, doi = {}, year = {2017}, } Article: popl17main-main4-p (type: Full Paper) doi:
	Shan, Chung-chieh	POPL '17: "Exact Bayesian Inference by ..." Exact Bayesian Inference by Symbolic Disintegration Chung-chieh Shan and Norman Ramsey (Indiana University, USA; Tufts University, USA) @InProceedings{POPL17p343, author = {Chung-chieh Shan and Norman Ramsey}, title = {Exact Bayesian Inference by Symbolic Disintegration}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {343-342}, doi = {}, year = {2017}, } Article: popl17main-main95-p (type: Full Paper) doi:
	Siek, Jeremy G.	POPL '17: "Big Types in Little Runtime: ..." Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek (Indiana University, USA) @InProceedings{POPL17p1063, author = {Michael M. Vitousek and Cameron Swords and Jeremy G. Siek}, title = {Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1063-1062}, doi = {}, year = {2017}, } Article: popl17main-main63-p (type: Full Paper) doi: POPL '17: "Automatically Generating the ..." Automatically Generating the Dynamic Semantics of Gradually Typed Languages Matteo Cimini and Jeremy G. Siek (Indiana University, USA) @InProceedings{POPL17p1095, author = {Matteo Cimini and Jeremy G. Siek}, title = {Automatically Generating the Dynamic Semantics of Gradually Typed Languages}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1095-1094}, doi = {}, year = {2017}, } Article: popl17main-main134-p (type: Full Paper) doi:
	Signoles, Julien	POPL '17: "Hypercollecting Semantics ..." Hypercollecting Semantics and Its Application to Static Analysis of Information Flow Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel (Stevens Institute of Technology, USA; CEA LIST, France; CentraleSupélec, France) @InProceedings{POPL17p1191, author = {Mounir Assaf and David A. Naumann and Julien Signoles and Éric Totel and Frédéric Tronel}, title = {Hypercollecting Semantics and Its Application to Static Analysis of Information Flow}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1191-1190}, doi = {}, year = {2017}, } Article: popl17main-main256-p (type: Full Paper) doi:
	Silva, Alexandra	POPL '17: "Cantor Meets Scott: Semantic ..." Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University College London, UK) @InProceedings{POPL17p823, author = {Steffen Smolka and Praveen Kumar and Nate Foster and Dexter Kozen and Alexandra Silva}, title = {Cantor Meets Scott: Semantic Foundations for Probabilistic Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {823-822}, doi = {}, year = {2017}, } Article: popl17main-main18-p (type: Full Paper) doi: POPL '17: "Learning Nominal Automata ..." Learning Nominal Automata Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michał Szynwelski (Radboud University Nijmegen, Netherlands; University College London, UK; University of Warsaw, Poland) @InProceedings{POPL17p887, author = {Joshua Moerman and Matteo Sammartino and Alexandra Silva and Bartek Klin and Michał Szynwelski}, title = {Learning Nominal Automata}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {887-886}, doi = {}, year = {2017}, } Article: popl17main-main209-p (type: Full Paper) doi:
	Singh, Gagandeep	POPL '17: "Fast Polyhedra Abstract Domain ..." Fast Polyhedra Abstract Domain Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) @InProceedings{POPL17p247, author = {Gagandeep Singh and Markus Püschel and Martin Vechev}, title = {Fast Polyhedra Abstract Domain}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {247-246}, doi = {}, year = {2017}, } Article: popl17main-main238-p (type: Full Paper) doi:
	Smaragdakis, Yannis	POPL '17: "Stream Fusion, to Completeness ..." Stream Fusion, to Completeness Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, and Yannis Smaragdakis (Tohoku University, Japan; University of Athens, Greece; Nessos IT, Greece) @InProceedings{POPL17p519, author = {Oleg Kiselyov and Aggelos Biboudis and Nick Palladinos and Yannis Smaragdakis}, title = {Stream Fusion, to Completeness}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {519-518}, doi = {}, year = {2017}, } Article: popl17main-main218-p (type: Full Paper) doi:
	Smolka, Steffen	POPL '17: "Cantor Meets Scott: Semantic ..." Cantor Meets Scott: Semantic Foundations for Probabilistic Networks Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University College London, UK) @InProceedings{POPL17p823, author = {Steffen Smolka and Praveen Kumar and Nate Foster and Dexter Kozen and Alexandra Silva}, title = {Cantor Meets Scott: Semantic Foundations for Probabilistic Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {823-822}, doi = {}, year = {2017}, } Article: popl17main-main18-p (type: Full Paper) doi:
	Solovyev, Alexey	POPL '17: "Rigorous Floating-Point Mixed-Precision ..." Rigorous Floating-Point Mixed-Precision Tuning Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić (University of Utah, USA) @InProceedings{POPL17p535, author = {Wei-Fan Chiang and Mark Baranowski and Ian Briggs and Alexey Solovyev and Ganesh Gopalakrishnan and Zvonimir Rakamarić}, title = {Rigorous Floating-Point Mixed-Precision Tuning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {535-534}, doi = {}, year = {2017}, } Article: popl17main-main41-p (type: Full Paper) doi:
	Sorensen, Tyler	POPL '17: "Automatically Comparing Memory ..." Automatically Comparing Memory Consistency Models John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides (Imperial College London, UK; University of Kent, UK) @InProceedings{POPL17p407, author = {John Wickerson and Mark Batty and Tyler Sorensen and George A. Constantinides}, title = {Automatically Comparing Memory Consistency Models}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {407-406}, doi = {}, year = {2017}, } Article: popl17main-main2-p (type: Full Paper) doi:
	Srikanth, Akhilesh	POPL '17: "Complexity Verification using ..." Complexity Verification using Guided Theorem Enumeration Akhilesh Srikanth, Burak Sahin, and William R. Harris (Georgia Institute of Technology, USA) @InProceedings{POPL17p919, author = {Akhilesh Srikanth and Burak Sahin and William R. Harris}, title = {Complexity Verification using Guided Theorem Enumeration}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {919-918}, doi = {}, year = {2017}, } Article: popl17main-main137-p (type: Full Paper) doi:
	Strub, Pierre-Yves	POPL '17: "Coupling Proofs Are Probabilistic ..." Coupling Proofs Are Probabilistic Product Programs Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; Inria, France; University of Pennsylvania, USA; École Polytechnique, France) @InProceedings{POPL17p375, author = {Gilles Barthe and Benjamin Grégoire and Justin Hsu and Pierre-Yves Strub}, title = {Coupling Proofs Are Probabilistic Product Programs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {375-374}, doi = {}, year = {2017}, } Article: popl17main-main290-p (type: Full Paper) doi:
	Su, Zhendong	POPL '17: "Context-Sensitive Data-Dependence ..." Context-Sensitive Data-Dependence Analysis via Linear Conjunctive Language Reachability Qirun Zhang and Zhendong Su (University of California at Davis, USA) @InProceedings{POPL17p583, author = {Qirun Zhang and Zhendong Su}, title = {Context-Sensitive Data-Dependence Analysis via Linear Conjunctive Language Reachability}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {583-582}, doi = {}, year = {2017}, } Article: popl17main-main58-p (type: Full Paper) doi:
	Subramanian, Kausik	POPL '17: "Genesis: Synthesizing Forwarding ..." Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks Kausik Subramanian, Loris D'Antoni, and Aditya Akella (University of Wisconsin-Madison, USA) @InProceedings{POPL17p839, author = {Kausik Subramanian and Loris D'Antoni and Aditya Akella}, title = {Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {839-838}, doi = {}, year = {2017}, } Article: popl17main-main35-p (type: Full Paper) doi:
	Svendsen, Kasper	POPL '17: "A Relational Model of Types-and-Effects ..." A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal (Aarhus University, Denmark; University of Cambridge, UK) @InProceedings{POPL17p439, author = {Morten Krogh-Jespersen and Kasper Svendsen and Lars Birkedal}, title = {A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {439-438}, doi = {}, year = {2017}, } Article: popl17main-main192-p (type: Full Paper) doi:
	Swamy, Nikhil	POPL '17: "Dijkstra Monads for Free ..." Dijkstra Monads for Free Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy (University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India) @InProceedings{POPL17p775, author = {Danel Ahman and Cătălin Hriţcu and Kenji Maillard and Guido Martínez and Gordon Plotkin and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy}, title = {Dijkstra Monads for Free}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {775-774}, doi = {}, year = {2017}, } Article: popl17main-main206-p (type: Full Paper) doi:
	Swords, Cameron	POPL '17: "Big Types in Little Runtime: ..." Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek (Indiana University, USA) @InProceedings{POPL17p1063, author = {Michael M. Vitousek and Cameron Swords and Jeremy G. Siek}, title = {Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1063-1062}, doi = {}, year = {2017}, } Article: popl17main-main63-p (type: Full Paper) doi:
	Szynwelski, Michał	POPL '17: "Learning Nominal Automata ..." Learning Nominal Automata Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michał Szynwelski (Radboud University Nijmegen, Netherlands; University College London, UK; University of Warsaw, Poland) @InProceedings{POPL17p887, author = {Joshua Moerman and Matteo Sammartino and Alexandra Silva and Bartek Klin and Michał Szynwelski}, title = {Learning Nominal Automata}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {887-886}, doi = {}, year = {2017}, } Article: popl17main-main209-p (type: Full Paper) doi:
	Tanter, Éric	POPL '17: "Gradual Refinement Types ..." Gradual Refinement Types Nico Lehmann and Éric Tanter (University of Chile, Chile) @InProceedings{POPL17p1079, author = {Nico Lehmann and Éric Tanter}, title = {Gradual Refinement Types}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1079-1078}, doi = {}, year = {2017}, } Article: popl17main-main102-p (type: Full Paper) doi:
	Timany, Amin	POPL '17: "Interactive Proofs in Higher-Order ..." Interactive Proofs in Higher-Order Concurrent Separation Logic Robbert Krebbers, Amin Timany, and Lars Birkedal (Delft University of Technology, Netherlands; KU Leuven, Belgium; Aarhus University, Denmark) @InProceedings{POPL17p423, author = {Robbert Krebbers and Amin Timany and Lars Birkedal}, title = {Interactive Proofs in Higher-Order Concurrent Separation Logic}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, } Article: popl17main-main99-p (type: Full Paper) doi:
	Toninho, Bernardo	POPL '17: "Fencing off Go: Liveness and ..." Fencing off Go: Liveness and Safety for Channel-Based Programming Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida (Imperial College London, UK) @InProceedings{POPL17p1047, author = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida}, title = {Fencing off Go: Liveness and Safety for Channel-Based Programming}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1047-1046}, doi = {}, year = {2017}, } Article: popl17main-main51-p (type: Full Paper) doi:
	Toruńczyk, Szymon	POPL '17: "LOIS: Syntax and Semantics ..." LOIS: Syntax and Semantics Eryk Kopczyński and Szymon Toruńczyk (University of Warsaw, Poland) @InProceedings{POPL17p855, author = {Eryk Kopczyński and Szymon Toruńczyk}, title = {LOIS: Syntax and Semantics}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {855-854}, doi = {}, year = {2017}, } Article: popl17main-main189-p (type: Full Paper) doi:
	Totel, Éric	POPL '17: "Hypercollecting Semantics ..." Hypercollecting Semantics and Its Application to Static Analysis of Information Flow Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel (Stevens Institute of Technology, USA; CEA LIST, France; CentraleSupélec, France) @InProceedings{POPL17p1191, author = {Mounir Assaf and David A. Naumann and Julien Signoles and Éric Totel and Frédéric Tronel}, title = {Hypercollecting Semantics and Its Application to Static Analysis of Information Flow}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1191-1190}, doi = {}, year = {2017}, } Article: popl17main-main256-p (type: Full Paper) doi:
	Tronel, Frédéric	POPL '17: "Hypercollecting Semantics ..." Hypercollecting Semantics and Its Application to Static Analysis of Information Flow Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel (Stevens Institute of Technology, USA; CEA LIST, France; CentraleSupélec, France) @InProceedings{POPL17p1191, author = {Mounir Assaf and David A. Naumann and Julien Signoles and Éric Totel and Frédéric Tronel}, title = {Hypercollecting Semantics and Its Application to Static Analysis of Information Flow}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1191-1190}, doi = {}, year = {2017}, } Article: popl17main-main256-p (type: Full Paper) doi:
	Turon, Aaron	POPL '17: "Rust: From POPL to Practice ..." Rust: From POPL to Practice (Keynote) Aaron Turon (Mozilla, USA) @InProceedings{POPL17p100, author = {Aaron Turon}, title = {Rust: From POPL to Practice (Keynote)}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {100-99}, doi = {}, year = {2017}, } Article: popl17key-key2-p (type: Invited Talk Abstract) doi:
	Vafeiadis, Viktor	POPL '17: "A Promising Semantics for ..." A Promising Semantics for Relaxed-Memory Concurrency Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) @InProceedings{POPL17p391, author = {Jeehoon Kang and Chung-Kil Hur and Ori Lahav and Viktor Vafeiadis and Derek Dreyer}, title = {A Promising Semantics for Relaxed-Memory Concurrency}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {391-390}, doi = {}, year = {2017}, } Article: popl17main-main65-p (type: Full Paper) doi:
	Valiron, Benoît	POPL '17: "The Geometry of Parallelism: ..." The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu (University of Bologna, Italy; Inria, France; CNRS, France; University of Paris Diderot, France; University of Paris-Saclay, France; University of Tokyo, Japan) @InProceedings{POPL17p1143, author = {Ugo Dal Lago and Claudia Faggian and Benoît Valiron and Akira Yoshimizu}, title = {The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1143-1142}, doi = {}, year = {2017}, } Article: popl17main-main113-p (type: Full Paper) doi:
	Veanes, Margus	POPL '17: "Monadic Second-Order Logic ..." Monadic Second-Order Logic on Finite Sequences Loris D'Antoni and Margus Veanes (University of Wisconsin-Madison, USA; Microsoft Research, USA) @InProceedings{POPL17p455, author = {Loris D'Antoni and Margus Veanes}, title = {Monadic Second-Order Logic on Finite Sequences}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {455-454}, doi = {}, year = {2017}, } Article: popl17main-main32-p (type: Full Paper) doi:
	Vechev, Martin	POPL '17: "Fast Polyhedra Abstract Domain ..." Fast Polyhedra Abstract Domain Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) @InProceedings{POPL17p247, author = {Gagandeep Singh and Markus Püschel and Martin Vechev}, title = {Fast Polyhedra Abstract Domain}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {247-246}, doi = {}, year = {2017}, } Article: popl17main-main238-p (type: Full Paper) doi: POPL '17: "Serializability for Eventual ..." Serializability for Eventual Consistency: Criterion, Analysis, and Applications Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev (ETH Zurich, Switzerland) @InProceedings{POPL17p711, author = {Lucas Brutschy and Dimitar Dimitrov and Peter Müller and Martin Vechev}, title = {Serializability for Eventual Consistency: Criterion, Analysis, and Applications}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {711-710}, doi = {}, year = {2017}, } Article: popl17main-main285-p (type: Full Paper) doi:
	Veith, Helmut	POPL '17: "A Short Counterexample Property ..." A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder (Vienna University of Technology, Austria) @InProceedings{POPL17p1015, author = {Igor Konnov and Marijana Lazić and Helmut Veith and Josef Widder}, title = {A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1015-1014}, doi = {}, year = {2017}, } Article: popl17main-main116-p (type: Full Paper) doi:
	Vitousek, Michael M.	POPL '17: "Big Types in Little Runtime: ..." Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek (Indiana University, USA) @InProceedings{POPL17p1063, author = {Michael M. Vitousek and Cameron Swords and Jeremy G. Siek}, title = {Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1063-1062}, doi = {}, year = {2017}, } Article: popl17main-main63-p (type: Full Paper) doi:
	Voronkov, Andrei	POPL '17: "Coming to Terms with Quantified ..." Coming to Terms with Quantified Reasoning Laura Kovács, Simon Robillard, and Andrei Voronkov (Vienna University of Technology, Austria; Chalmers University of Technology, Sweden; University of Manchester, UK) @InProceedings{POPL17p487, author = {Laura Kovács and Simon Robillard and Andrei Voronkov}, title = {Coming to Terms with Quantified Reasoning}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {487-486}, doi = {}, year = {2017}, } Article: popl17main-main253-p (type: Full Paper) doi:
	Voysey, Ian	POPL '17: "Hazelnut: A Bidirectionally ..." Hazelnut: A Bidirectionally Typed Structure Editor Calculus Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer (Carnegie Mellon University, USA; Oregon State University, USA; University of Colorado at Boulder, USA) @InProceedings{POPL17p295, author = {Cyrus Omar and Ian Voysey and Michael Hilton and Jonathan Aldrich and Matthew A. Hammer}, title = {Hazelnut: A Bidirectionally Typed Structure Editor Calculus}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {295-294}, doi = {}, year = {2017}, } Article: popl17main-main319-p (type: Full Paper) doi:
	Wang, Yuepeng	POPL '17: "Component-Based Synthesis ..." Component-Based Synthesis for Complex APIs Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps (University of Texas at Austin, USA; University of Wisconsin-Madison, USA) @InProceedings{POPL17p871, author = {Yu Feng and Ruben Martins and Yuepeng Wang and Isil Dillig and Thomas W. Reps}, title = {Component-Based Synthesis for Complex APIs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {871-870}, doi = {}, year = {2017}, } Article: popl17main-main93-p (type: Full Paper) doi:
	Weirich, Stephanie	POPL '17: "The Influence of Dependent ..." The Influence of Dependent Types (Keynote) Stephanie Weirich (University of Pennsylvania, USA) @InProceedings{POPL17p1, author = {Stephanie Weirich}, title = {The Influence of Dependent Types (Keynote)}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2017}, } Article: popl17key-key1-p (type: Invited Talk Abstract) doi:
	Weng, Shu-Chun	POPL '17: "Towards Automatic Resource ..." Towards Automatic Resource Bound Analysis for OCaml Jan Hoffmann, Ankush Das, and Shu-Chun Weng (Carnegie Mellon University, USA; Yale University, USA) @InProceedings{POPL17p599, author = {Jan Hoffmann and Ankush Das and Shu-Chun Weng}, title = {Towards Automatic Resource Bound Analysis for OCaml}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {599-598}, doi = {}, year = {2017}, } Article: popl17main-main17-p (type: Full Paper) doi:
	Wickerson, John	POPL '17: "Automatically Comparing Memory ..." Automatically Comparing Memory Consistency Models John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides (Imperial College London, UK; University of Kent, UK) @InProceedings{POPL17p407, author = {John Wickerson and Mark Batty and Tyler Sorensen and George A. Constantinides}, title = {Automatically Comparing Memory Consistency Models}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {407-406}, doi = {}, year = {2017}, } Article: popl17main-main2-p (type: Full Paper) doi:
	Widder, Josef	POPL '17: "A Short Counterexample Property ..." A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder (Vienna University of Technology, Austria) @InProceedings{POPL17p1015, author = {Igor Konnov and Marijana Lazić and Helmut Veith and Josef Widder}, title = {A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1015-1014}, doi = {}, year = {2017}, } Article: popl17main-main116-p (type: Full Paper) doi:
	Wilson, Todd	POPL '17: "Computational Higher-Dimensional ..." Computational Higher-Dimensional Type Theory Carlo Angiuli, Robert Harper, and Todd Wilson (Carnegie Mellon University, USA; California State University at Fresno, USA) @InProceedings{POPL17p967, author = {Carlo Angiuli and Robert Harper and Todd Wilson}, title = {Computational Higher-Dimensional Type Theory}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {967-966}, doi = {}, year = {2017}, } Article: popl17main-main126-p (type: Full Paper) doi:
	Wu, Xiaodi	POPL '17: "Invariants of Quantum Programs: ..." Invariants of Quantum Programs: Characterisations and Generation Mingsheng Ying, Shenggang Ying, and Xiaodi Wu (University of Technology Sydney, Australia; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Oregon, USA) @InProceedings{POPL17p1127, author = {Mingsheng Ying and Shenggang Ying and Xiaodi Wu}, title = {Invariants of Quantum Programs: Characterisations and Generation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1127-1126}, doi = {}, year = {2017}, } Article: popl17main-main10-p (type: Full Paper) doi:
	Xia, Li-yao	POPL '17: "Beginner's Luck: A Language ..." Beginner's Luck: A Language for Property-Based Generators Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia (University of Pennsylvania, USA; Inria, France; ENS, France; Chalmers University of Technology, Sweden) @InProceedings{POPL17p327, author = {Leonidas Lampropoulos and Diane Gallois-Wong and Cătălin Hriţcu and John Hughes and Benjamin C. Pierce and Li-yao Xia}, title = {Beginner's Luck: A Language for Property-Based Generators}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {327-326}, doi = {}, year = {2017}, } Article: popl17main-main152-p (type: Full Paper) doi:
	Ying, Mingsheng	POPL '17: "Invariants of Quantum Programs: ..." Invariants of Quantum Programs: Characterisations and Generation Mingsheng Ying, Shenggang Ying, and Xiaodi Wu (University of Technology Sydney, Australia; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Oregon, USA) @InProceedings{POPL17p1127, author = {Mingsheng Ying and Shenggang Ying and Xiaodi Wu}, title = {Invariants of Quantum Programs: Characterisations and Generation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1127-1126}, doi = {}, year = {2017}, } Article: popl17main-main10-p (type: Full Paper) doi:
	Ying, Shenggang	POPL '17: "Invariants of Quantum Programs: ..." Invariants of Quantum Programs: Characterisations and Generation Mingsheng Ying, Shenggang Ying, and Xiaodi Wu (University of Technology Sydney, Australia; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Oregon, USA) @InProceedings{POPL17p1127, author = {Mingsheng Ying and Shenggang Ying and Xiaodi Wu}, title = {Invariants of Quantum Programs: Characterisations and Generation}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1127-1126}, doi = {}, year = {2017}, } Article: popl17main-main10-p (type: Full Paper) doi:
	Yoshida, Nobuko	POPL '17: "Fencing off Go: Liveness and ..." Fencing off Go: Liveness and Safety for Channel-Based Programming Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida (Imperial College London, UK) @InProceedings{POPL17p1047, author = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida}, title = {Fencing off Go: Liveness and Safety for Channel-Based Programming}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1047-1046}, doi = {}, year = {2017}, } Article: popl17main-main51-p (type: Full Paper) doi:
	Yoshimizu, Akira	POPL '17: "The Geometry of Parallelism: ..." The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu (University of Bologna, Italy; Inria, France; CNRS, France; University of Paris Diderot, France; University of Paris-Saclay, France; University of Tokyo, Japan) @InProceedings{POPL17p1143, author = {Ugo Dal Lago and Claudia Faggian and Benoît Valiron and Akira Yoshimizu}, title = {The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1143-1142}, doi = {}, year = {2017}, } Article: popl17main-main113-p (type: Full Paper) doi:
	Yu, Tingting	POPL '17: "Analyzing Divergence in Bisimulation ..." Analyzing Divergence in Bisimulation Semantics Xinxin Liu, Tingting Yu, and Wenhui Zhang (Institute of Software at Chinese Academy of Sciences, China) @InProceedings{POPL17p1031, author = {Xinxin Liu and Tingting Yu and Wenhui Zhang}, title = {Analyzing Divergence in Bisimulation Semantics}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1031-1030}, doi = {}, year = {2017}, } Article: popl17main-main158-p (type: Full Paper) doi:
	Zdancewic, Steve	POPL '17: "QWIRE: A Core Language for ..." QWIRE: A Core Language for Quantum Circuits Jennifer Paykin, Robert Rand, and Steve Zdancewic (University of Pennsylvania, USA) @InProceedings{POPL17p1159, author = {Jennifer Paykin and Robert Rand and Steve Zdancewic}, title = {QWIRE: A Core Language for Quantum Circuits}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1159-1158}, doi = {}, year = {2017}, } Article: popl17main-main278-p (type: Full Paper) doi:
	Zhang, Danfeng	POPL '17: "LightDP: Towards Automating ..." LightDP: Towards Automating Differential Privacy Proofs Danfeng Zhang and Daniel Kifer (Pennsylvania State University, USA) @InProceedings{POPL17p1207, author = {Danfeng Zhang and Daniel Kifer}, title = {LightDP: Towards Automating Differential Privacy Proofs}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1207-1206}, doi = {}, year = {2017}, } Article: popl17main-main234-p (type: Full Paper) doi:
	Zhang, Qirun	POPL '17: "Context-Sensitive Data-Dependence ..." Context-Sensitive Data-Dependence Analysis via Linear Conjunctive Language Reachability Qirun Zhang and Zhendong Su (University of California at Davis, USA) @InProceedings{POPL17p583, author = {Qirun Zhang and Zhendong Su}, title = {Context-Sensitive Data-Dependence Analysis via Linear Conjunctive Language Reachability}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {583-582}, doi = {}, year = {2017}, } Article: popl17main-main58-p (type: Full Paper) doi:
	Zhang, Wenhui	POPL '17: "Analyzing Divergence in Bisimulation ..." Analyzing Divergence in Bisimulation Semantics Xinxin Liu, Tingting Yu, and Wenhui Zhang (Institute of Software at Chinese Academy of Sciences, China) @InProceedings{POPL17p1031, author = {Xinxin Liu and Tingting Yu and Wenhui Zhang}, title = {Analyzing Divergence in Bisimulation Semantics}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {1031-1030}, doi = {}, year = {2017}, } Article: popl17main-main158-p (type: Full Paper) doi:
	Žikelić, Ðorđe	POPL '17: "Stochastic Invariants for ..." Stochastic Invariants for Probabilistic Termination Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić (IST Austria, Austria; University of Cambridge, UK) @InProceedings{POPL17p359, author = {Krishnendu Chatterjee and Petr Novotný and Ðorđe Žikelić}, title = {Stochastic Invariants for Probabilistic Termination}, booktitle = {Proc.\ POPL}, publisher = {ACM}, pages = {359-358}, doi = {}, year = {2017}, } Article: popl17main-main182-p (type: Full Paper) doi:

206 authors

proc time: 0.22