| |
Abel, Andreas
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Decidability of Conversion ..."
Decidability of Conversion for Type Theory in Type Theory
Andreas Abel, Joakim Öhman, and Andrea Vezzosi
(University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden)
 Publisher's Version
Artifacts Functional
Article: popl18main-p128-p doi:10.1145/3158111
|
| |
Abraham, Ittai |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..."
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p124-p doi:10.1145/3158136
|
| |
Agrawal, Sheshansh |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Lexicographic Ranking Supermartingales: ..."
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný
(IIT Bombay, India; IST Austria, Austria)
Publisher's Version
Artifacts Functional
Article: popl18main-p131-p doi:10.1145/3158122
|
| |
Ahman, Danel |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..."
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p134-p doi:10.1145/3158153
Proc. ACM Program. Lang., vol. 2, issue POPL: "Handling Fibred Algebraic ..."
Handling Fibred Algebraic Effects
Danel Ahman
(Inria, France)
Publisher's Version
Article: popl18main-p68-p doi:10.1145/3158095
|
| |
Ahmed, Amal |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..."
Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible
William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed
(Northeastern University, USA; Ochanomizu University, Japan)
Publisher's Version
Article: popl18main-p51-p doi:10.1145/3158110
Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..."
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek
(Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
Publisher's Version
Article: popl18main-p31-p doi:10.1145/3158137
|
| |
Aiken, Alex |
Proc. ACM Program. Lang., vol. 2, issue POPL: "On Automatically Proving the ..."
On Automatically Proving the Correctness of math.h Implementations
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India)
Publisher's Version
Article: popl18main-p43-p doi:10.1145/3158135
|
| |
Albarghouthi, Aws |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Coupling Proofs ..."
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi and Justin Hsu
(University of Wisconsin-Madison, USA; University College London, UK)
Publisher's Version
Article: popl18main-p172-p doi:10.1145/3158146
|
| |
Amin, Nada |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Collapsing Towers of Interpreters ..."
Collapsing Towers of Interpreters
Nada Amin and Tiark Rompf
(University of Cambridge, UK; Purdue University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p33-p doi:10.1145/3158140
|
| |
Bach Poulsen, Casper
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Portland State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p277-p doi:10.1145/3158104
|
| |
Bao, Wenlei |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..."
Analytical Modeling of Cache Behavior for Affine Programs
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan
(Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
Publisher's Version
Article: popl18main-p175-p doi:10.1145/3158120
|
| |
Barthe, Gilles |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..."
Monadic Refinements for Relational Cost Analysis
Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger
(Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl18main-p94-p doi:10.1145/3158124
Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..."
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)
Publisher's Version
Artifacts Functional
Article: popl18main-p106-p doi:10.1145/3158145
|
| |
Bernardy, Jean-Philippe |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..."
Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p2-p doi:10.1145/3158093
|
| |
Biboudis, Aggelos |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..."
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p247-p doi:10.1145/3158130
|
| |
Biernacki, Dariusz |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..."
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Artifacts Functional
Article: popl18main-p160-p doi:10.1145/3158096
|
| |
Birkedal, Lars |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..."
A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal
(KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark)
Publisher's Version
Artifacts Functional
Article: popl18main-p27-p doi:10.1145/3158152
|
| |
Blanvillain, Olivier |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..."
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p247-p doi:10.1145/3158130
|
| |
Bodik, Rastislav |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Bonsai: Synthesis-Based Reasoning ..."
Bonsai: Synthesis-Based Reasoning for Type Systems
Kartik Chandra and Rastislav Bodik
(Henry M. Gunn High School, USA; Stanford University, USA; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p282-p doi:10.1145/3158150
|
| |
Boespflug, Mathieu |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..."
Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p2-p doi:10.1145/3158093
|
| |
Bowman, William J. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..."
Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible
William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed
(Northeastern University, USA; Ochanomizu University, Japan)
Publisher's Version
Article: popl18main-p51-p doi:10.1145/3158110
|
| |
Breck, Jason |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..."
Non-linear Reasoning for Invariant Synthesis
Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps
(Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p201-p doi:10.1145/3158142
|
| |
Brown, Matt |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Jones-Optimal Partial Evaluation ..."
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p189-p doi:10.1145/3158102
|
| |
Cai, Yufei
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Campora, John Peter |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..."
Migrating Gradual Types
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p239-p doi:10.1145/3158103
|
| |
Capriotti, Paolo |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Univalent Higher Categories ..."
Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti and Nicolai Kraus
(University of Nottingham, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p216-p doi:10.1145/3158132
|
| |
Cathcart Burn, Toby |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Higher-Order Constrained Horn ..."
Higher-Order Constrained Horn Clauses for Verification
Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay
(University of Oxford, UK; University of Bristol, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p253-p doi:10.1145/3158099
|
| |
Chalupa, Marek |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..."
Data-Centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya
(Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
Publisher's Version
Article: popl18main-p88-p doi:10.1145/3158119
|
| |
Chandra, Kartik |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Bonsai: Synthesis-Based Reasoning ..."
Bonsai: Synthesis-Based Reasoning for Type Systems
Kartik Chandra and Rastislav Bodik
(Henry M. Gunn High School, USA; Stanford University, USA; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p282-p doi:10.1145/3158150
|
| |
Chang, Stephen |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Symbolic Types for Lenient ..."
Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, and Emina Torlak
(Northeastern University, USA; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p180-p doi:10.1145/3158128
|
| |
Chatterjee, Krishnendu |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Optimal Dyck Reachability ..."
Optimal Dyck Reachability for Data-Dependence and Alias Analysis
Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Publisher's Version
Artifacts Functional
Article: popl18main-p187-p doi:10.1145/3158118
Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..."
Data-Centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya
(Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
Publisher's Version
Article: popl18main-p88-p doi:10.1145/3158119
Proc. ACM Program. Lang., vol. 2, issue POPL: "Lexicographic Ranking Supermartingales: ..."
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný
(IIT Bombay, India; IST Austria, Austria)
Publisher's Version
Artifacts Functional
Article: popl18main-p131-p doi:10.1145/3158122
|
| |
Chen, Sheng |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..."
Migrating Gradual Types
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p239-p doi:10.1145/3158103
|
| |
Chen, Taolue |
Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..."
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
(University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
Publisher's Version
Article: popl18main-p264-p doi:10.1145/3158091
|
| |
Chen, Yan |
Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..."
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
(University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
Publisher's Version
Article: popl18main-p264-p doi:10.1145/3158091
|
| |
Chin, Wei-Ngan |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..."
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Publisher's Version
Artifacts Functional
Article: popl18main-p281-p doi:10.1145/3158097
|
| |
Choudhary, Bhavya |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Optimal Dyck Reachability ..."
Optimal Dyck Reachability for Data-Dependence and Alias Analysis
Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Publisher's Version
Artifacts Functional
Article: popl18main-p187-p doi:10.1145/3158118
|
| |
Choudhury, Vikraman |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..."
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p1-p doi:10.1145/3158141
|
| |
Clairambault, Pierre |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linearity in Higher-Order ..."
Linearity in Higher-Order Recursion Schemes
Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Inria, France; Aix-Marseille University, France; ENSAM, France; University of Toulon, France; University of Oxford, UK)
Publisher's Version
Article: popl18main-p178-p doi:10.1145/3158127
|
| |
Cong, Youyou |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..."
Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible
William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed
(Northeastern University, USA; Ochanomizu University, Japan)
Publisher's Version
Article: popl18main-p51-p doi:10.1145/3158110
|
| |
Cook, William R. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..."
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Article: popl18main-p19-p doi:10.1145/3158144
|
| |
Cyphert, John |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..."
Non-linear Reasoning for Invariant Synthesis
Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps
(Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p201-p doi:10.1145/3158142
|
| |
Danielsson, Nils Anders
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Up-to Techniques using Sized ..."
Up-to Techniques using Sized Types
Nils Anders Danielsson
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p181-p doi:10.1145/3158131
|
| |
Deacon, Will |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..."
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p5-p doi:10.1145/3158107
|
| |
De Araújo, Marcus R. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..."
Inference of Static Semantics for Incomplete C Programs
Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil)
Publisher's Version
Artifacts Functional
Article: popl18main-p110-p doi:10.1145/3158117
|
| |
Devriese, Dominique |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Parametricity versus the Universal ..."
Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
Publisher's Version
Article: popl18main-p46-p doi:10.1145/3158126
|
| |
Dillig, Isil |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..."
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Article: popl18main-p19-p doi:10.1145/3158144
Proc. ACM Program. Lang., vol. 2, issue POPL: "Program Synthesis using Abstraction ..."
Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig, and Rishabh Singh
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Article: popl18main-p20-p doi:10.1145/3158151
|
| |
Dongol, Brijesh |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Transactions in Relaxed Memory ..."
Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, and James Riely
(Brunel University London, UK; DePaul University, USA)
Publisher's Version
Article: popl18main-p154-p doi:10.1145/3158106
|
| |
Dreyer, Derek |
Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..."
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer
(MPI-SWS, Germany; Delft University of Technology, Netherlands)
Publisher's Version
Artifacts Functional
Article: popl18main-p202-p doi:10.1145/3158154
|
| |
Ehrhard, Thomas
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Measurable Cones and Stable, ..."
Measurable Cones and Stable, Measurable Functions: A Model for Probabilistic Higher-Order Programming
Thomas Ehrhard, Michele Pagani, and Christine Tasson
(University of Paris Diderot, France; CNRS, France)
Publisher's Version
Article: popl18main-p165-p doi:10.1145/3158147
|
| |
Emmi, Michael |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Sound, Complete, and Tractable ..."
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Michael Emmi and Constantin Enea
(SRI International, USA; University of Paris Diderot, France; CNRS, France)
Publisher's Version
Article: popl18main-p59-p doi:10.1145/3158113
|
| |
Enea, Constantin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Sound, Complete, and Tractable ..."
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Michael Emmi and Constantin Enea
(SRI International, USA; University of Paris Diderot, France; CNRS, France)
Publisher's Version
Article: popl18main-p59-p doi:10.1145/3158113
|
| |
Erwig, Martin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..."
Migrating Gradual Types
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p239-p doi:10.1145/3158103
|
| |
Espitau, Thomas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..."
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)
Publisher's Version
Artifacts Functional
Article: popl18main-p106-p doi:10.1145/3158145
|
| |
Farzan, Azadeh
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Strategy Synthesis for Linear ..."
Strategy Synthesis for Linear Arithmetic Games
Azadeh Farzan and Zachary Kincaid
(University of Toronto, Canada; Princeton University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p207-p doi:10.1145/3158149
|
| |
Feng, Xinyu |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Progress of Concurrent Objects ..."
Progress of Concurrent Objects with Partial Methods
Hongjin Liang and Xinyu Feng
(Nanjing University, China; University of Science and Technology of China, China)
Publisher's Version
Article: popl18main-p96-p doi:10.1145/3158108
|
| |
Fisher, Kathleen |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..."
Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p18-p doi:10.1145/3158089
|
| |
Flückiger, Olivier |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..."
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek
(Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
Publisher's Version
Article: popl18main-p31-p doi:10.1145/3158137
|
| |
Flur, Shaked |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..."
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p5-p doi:10.1145/3158107
|
| |
Fournet, Cédric |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..."
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p134-p doi:10.1145/3158153
|
| |
Fragoso Santos, José |
Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..."
JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Artifacts Functional
Article: popl18main-p276-p doi:10.1145/3158138
|
| |
French, Jon |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..."
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p5-p doi:10.1145/3158107
|
| |
Gaboardi, Marco
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..."
Monadic Refinements for Relational Cost Analysis
Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger
(Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl18main-p94-p doi:10.1145/3158124
|
| |
Gardner, Philippa |
Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..."
JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Artifacts Functional
Article: popl18main-p276-p doi:10.1145/3158138
|
| |
Garg, Deepak |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..."
Monadic Refinements for Relational Cost Analysis
Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger
(Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl18main-p94-p doi:10.1145/3158124
|
| |
Ghahramani, Zoubin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Gilray, Thomas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..."
Soft Contract Verification for Higher-Order Stateful Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland, USA; Indiana University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p197-p doi:10.1145/3158139
|
| |
Goel, Aviral |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..."
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek
(Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
Publisher's Version
Article: popl18main-p31-p doi:10.1145/3158137
|
| |
Golan-Gueta, Guy |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..."
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p124-p doi:10.1145/3158136
|
| |
Grégoire, Benjamin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..."
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)
Publisher's Version
Artifacts Functional
Article: popl18main-p106-p doi:10.1145/3158145
|
| |
Grellois, Charles |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linearity in Higher-Order ..."
Linearity in Higher-Order Recursion Schemes
Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Inria, France; Aix-Marseille University, France; ENSAM, France; University of Toulon, France; University of Oxford, UK)
Publisher's Version
Article: popl18main-p178-p doi:10.1145/3158127
|
| |
Grossman, Shelly |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..."
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p124-p doi:10.1145/3158136
|
| |
Hague, Matthew
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..."
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
(University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
Publisher's Version
Article: popl18main-p264-p doi:10.1145/3158091
|
| |
Heunen, Chris |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Hoenicke, Jochen |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..."
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p145-p doi:10.1145/3158114
|
| |
Holík, Lukáš |
Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..."
String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p266-p doi:10.1145/3158092
|
| |
Hriţcu, Cătălin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..."
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p134-p doi:10.1145/3158153
|
| |
Hsu, Justin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..."
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)
Publisher's Version
Artifacts Functional
Article: popl18main-p106-p doi:10.1145/3158145
Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Coupling Proofs ..."
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi and Justin Hsu
(University of Wisconsin-Madison, USA; University College London, UK)
Publisher's Version
Article: popl18main-p172-p doi:10.1145/3158146
|
| |
Hu, Zhenjiang |
Proc. ACM Program. Lang., vol. 2, issue POPL: "An Axiomatic Basis for Bidirectional ..."
An Axiomatic Basis for Bidirectional Programming
Hsiang-Shang Ko and Zhenjiang Hu
(National Institute of Informatics, Japan)
Publisher's Version
Artifacts Functional
Article: popl18main-p3-p doi:10.1145/3158129
|
| |
Inala, Jeevana Priya
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "WebRelate: Integrating Web ..."
WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala and Rishabh Singh
(Massachusetts Institute of Technology, USA; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p114-p doi:10.1145/3158090
|
| |
Jagadeesan, Radha
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Transactions in Relaxed Memory ..."
Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, and James Riely
(Brunel University London, UK; DePaul University, USA)
Publisher's Version
Article: popl18main-p154-p doi:10.1145/3158106
|
| |
Jagannathan, Suresh |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..."
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan
(Purdue University, USA)
Publisher's Version
Article: popl18main-p209-p doi:10.1145/3158115
|
| |
Janků, Petr |
Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..."
String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p266-p doi:10.1145/3158092
|
| |
Jhala, Ranjit |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..."
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p1-p doi:10.1145/3158141
|
| |
Jourdan, Jacques-Henri |
Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..."
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer
(MPI-SWS, Germany; Delft University of Technology, Netherlands)
Publisher's Version
Artifacts Functional
Article: popl18main-p202-p doi:10.1145/3158154
|
| |
Jung, Ralf |
Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..."
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer
(MPI-SWS, Germany; Delft University of Technology, Netherlands)
Publisher's Version
Artifacts Functional
Article: popl18main-p202-p doi:10.1145/3158154
|
| |
Kaki, Gowtham
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..."
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan
(Purdue University, USA)
Publisher's Version
Article: popl18main-p209-p doi:10.1145/3158115
|
| |
Kaminski, Benjamin Lucien |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..."
A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen
(Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
Publisher's Version
Article: popl18main-p53-p doi:10.1145/3158121
|
| |
Kammar, Ohad |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Katoen, Joost-Pieter |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..."
A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen
(Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
Publisher's Version
Article: popl18main-p53-p doi:10.1145/3158121
|
| |
Khoo, Siau-Cheng |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..."
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Publisher's Version
Artifacts Functional
Article: popl18main-p281-p doi:10.1145/3158097
|
| |
Kincaid, Zachary |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..."
Non-linear Reasoning for Invariant Synthesis
Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps
(Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p201-p doi:10.1145/3158142
Proc. ACM Program. Lang., vol. 2, issue POPL: "Strategy Synthesis for Linear ..."
Strategy Synthesis for Linear Arithmetic Games
Azadeh Farzan and Zachary Kincaid
(University of Toronto, Canada; Princeton University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p207-p doi:10.1145/3158149
|
| |
Knauth, Alex |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Symbolic Types for Lenient ..."
Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, and Emina Torlak
(Northeastern University, USA; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p180-p doi:10.1145/3158128
|
| |
Ko, Hsiang-Shang |
Proc. ACM Program. Lang., vol. 2, issue POPL: "An Axiomatic Basis for Bidirectional ..."
An Axiomatic Basis for Bidirectional Programming
Hsiang-Shang Ko and Zhenjiang Hu
(National Institute of Informatics, Japan)
Publisher's Version
Artifacts Functional
Article: popl18main-p3-p doi:10.1145/3158129
|
| |
Koch, Christoph E. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..."
Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p285-p doi:10.1145/3158101
|
| |
Kokologiannakis, Michalis |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..."
Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis
(National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany)
Publisher's Version
Artifacts Functional
Article: popl18main-p80-p doi:10.1145/3158105
|
| |
Kraus, Nicolai |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Univalent Higher Categories ..."
Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti and Nicolai Kraus
(University of Nottingham, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p216-p doi:10.1145/3158132
|
| |
Krebbers, Robbert |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Portland State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p277-p doi:10.1145/3158104
Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..."
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer
(MPI-SWS, Germany; Delft University of Technology, Netherlands)
Publisher's Version
Artifacts Functional
Article: popl18main-p202-p doi:10.1145/3158154
|
| |
Krishna, Siddharth |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Go with the Flow: Compositional ..."
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, and Thomas Wies
(New York University, USA)
Publisher's Version
Article: popl18main-p190-p doi:10.1145/3158125
|
| |
Krishnamoorthy, Sriram |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..."
Analytical Modeling of Cache Behavior for Affine Programs
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan
(Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
Publisher's Version
Article: popl18main-p175-p doi:10.1145/3158120
|
| |
Krogh-Jespersen, Morten |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..."
A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal
(KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark)
Publisher's Version
Artifacts Functional
Article: popl18main-p27-p doi:10.1145/3158152
|
| |
Kunčar, Ondřej |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Safety and Conservativity ..."
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Ondřej Kunčar and Andrei Popescu
(TU Munich, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania)
Publisher's Version
Article: popl18main-p50-p doi:10.1145/3158112
|
| |
Lahav, Ori
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..."
Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis
(National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany)
Publisher's Version
Artifacts Functional
Article: popl18main-p80-p doi:10.1145/3158105
|
| |
Lahiri, Shuvendu K. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..."
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Article: popl18main-p19-p doi:10.1145/3158144
|
| |
Lampropoulos, Leonidas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Generating Good Generators ..."
Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce
(University of Pennsylvania, USA; Princeton University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p170-p doi:10.1145/3158133
|
| |
Le, Ton Chanh |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..."
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Publisher's Version
Artifacts Functional
Article: popl18main-p281-p doi:10.1145/3158097
|
| |
Lee, Wonyeol |
Proc. ACM Program. Lang., vol. 2, issue POPL: "On Automatically Proving the ..."
On Automatically Proving the Correctness of math.h Implementations
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India)
Publisher's Version
Article: popl18main-p43-p doi:10.1145/3158135
|
| |
Li, Yangjia |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Algorithmic Analysis of Termination ..."
Algorithmic Analysis of Termination Problems for Quantum Programs
Yangjia Li and Mingsheng Ying
(Institute of Software at Chinese Academy of Sciences, China; University of Technology Sydney, Australia; Tsinghua University, China)
Publisher's Version
Article: popl18main-p47-p doi:10.1145/3158123
|
| |
Liang, Hongjin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Progress of Concurrent Objects ..."
Progress of Concurrent Objects with Partial Methods
Hongjin Liang and Xinyu Feng
(Nanjing University, China; University of Science and Technology of China, China)
Publisher's Version
Article: popl18main-p96-p doi:10.1145/3158108
|
| |
Lin, Anthony W. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..."
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
(University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
Publisher's Version
Article: popl18main-p264-p doi:10.1145/3158091
Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..."
String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p266-p doi:10.1145/3158092
|
| |
Liu, Fengyun |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..."
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p247-p doi:10.1145/3158130
|
| |
Löding, Christof |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Foundations for Natural Proofs ..."
Foundations for Natural Proofs and Quantifier Instantiation
Christof Löding, P. Madhusudan, and Lucas Peña
(RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p99-p doi:10.1145/3158098
|
| |
Losa, Giuliano |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..."
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p145-p doi:10.1145/3158114
|
| |
Madhusudan, P.
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Foundations for Natural Proofs ..."
Foundations for Natural Proofs and Quantifier Instantiation
Christof Löding, P. Madhusudan, and Lucas Peña
(RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p99-p doi:10.1145/3158098
|
| |
Maillard, Kenji |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..."
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p134-p doi:10.1145/3158153
|
| |
Majumdar, Rupak |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Why Is Random Testing Effective ..."
Why Is Random Testing Effective for Partition Tolerance Bugs?
Rupak Majumdar and Filip Niksic
(MPI-SWS, Germany)
Publisher's Version
Article: popl18main-p141-p doi:10.1145/3158134
|
| |
Maksimović, Petar |
Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..."
JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Artifacts Functional
Article: popl18main-p276-p doi:10.1145/3158138
|
| |
Mazza, Damiano |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Polyadic Approximations, Fibrations ..."
Polyadic Approximations, Fibrations and Intersection Types
Damiano Mazza, Luc Pellissier, and Pierre Vial
(CNRS, France; University of Paris 13, France; University of Paris Diderot, France)
Publisher's Version
Article: popl18main-p265-p doi:10.1145/3158094
|
| |
McIver, Annabelle |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..."
A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen
(Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
Publisher's Version
Article: popl18main-p53-p doi:10.1145/3158121
|
| |
Melo, Leandro T. C. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..."
Inference of Static Semantics for Incomplete C Programs
Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil)
Publisher's Version
Artifacts Functional
Article: popl18main-p110-p doi:10.1145/3158117
|
| |
Michalevsky, Yan |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..."
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p124-p doi:10.1145/3158136
|
| |
Miller, Heather |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..."
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p247-p doi:10.1145/3158130
|
| |
Miltner, Anders |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..."
Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p18-p doi:10.1145/3158089
|
| |
Morgan, Carroll |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..."
A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen
(Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
Publisher's Version
Article: popl18main-p53-p doi:10.1145/3158121
|
| |
Moss, Sean K. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Murawski, Andrzej S. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linearity in Higher-Order ..."
Linearity in Higher-Order Recursion Schemes
Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Inria, France; Aix-Marseille University, France; ENSAM, France; University of Toulon, France; University of Oxford, UK)
Publisher's Version
Article: popl18main-p178-p doi:10.1145/3158127
|
| |
Nagar, Kartik
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..."
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan
(Purdue University, USA)
Publisher's Version
Article: popl18main-p209-p doi:10.1145/3158115
|
| |
Najafzadeh, Mahsa |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..."
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan
(Purdue University, USA)
Publisher's Version
Article: popl18main-p209-p doi:10.1145/3158115
|
| |
Naudžiūnienė, Daiva |
Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..."
JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Artifacts Functional
Article: popl18main-p276-p doi:10.1145/3158138
|
| |
Newton, Ryan R. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..."
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p1-p doi:10.1145/3158141
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..."
Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p2-p doi:10.1145/3158093
|
| |
Nguyễn, Phúc C. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..."
Soft Contract Verification for Higher-Order Stateful Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland, USA; Indiana University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p197-p doi:10.1145/3158139
|
| |
Niksic, Filip |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Why Is Random Testing Effective ..."
Why Is Random Testing Effective for Partition Tolerance Bugs?
Rupak Majumdar and Filip Niksic
(MPI-SWS, Germany)
Publisher's Version
Article: popl18main-p141-p doi:10.1145/3158134
|
| |
Novotný, Petr |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Lexicographic Ranking Supermartingales: ..."
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný
(IIT Bombay, India; IST Austria, Austria)
Publisher's Version
Artifacts Functional
Article: popl18main-p131-p doi:10.1145/3158122
|
| |
Odersky, Martin
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..."
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p247-p doi:10.1145/3158130
|
| |
Öhman, Joakim |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Decidability of Conversion ..."
Decidability of Conversion for Type Theory in Type Theory
Andreas Abel, Joakim Öhman, and Andrea Vezzosi
(University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p128-p doi:10.1145/3158111
|
| |
Ong, C.-H. Luke |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Higher-Order Constrained Horn ..."
Higher-Order Constrained Horn Clauses for Verification
Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay
(University of Oxford, UK; University of Bristol, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p253-p doi:10.1145/3158099
|
| |
Ostermann, Klaus |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Padon, Oded
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..."
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p145-p doi:10.1145/3158114
|
| |
Pagani, Michele |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Measurable Cones and Stable, ..."
Measurable Cones and Stable, Measurable Functions: A Model for Probabilistic Higher-Order Programming
Thomas Ehrhard, Michele Pagani, and Christine Tasson
(University of Paris Diderot, France; CNRS, France)
Publisher's Version
Article: popl18main-p165-p doi:10.1145/3158147
|
| |
Palsberg, Jens |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Jones-Optimal Partial Evaluation ..."
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p189-p doi:10.1145/3158102
|
| |
Paraskevopoulou, Zoe |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Generating Good Generators ..."
Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce
(University of Pennsylvania, USA; Princeton University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p170-p doi:10.1145/3158133
|
| |
Parreaux, Lionel |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..."
Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p285-p doi:10.1145/3158101
|
| |
Patrignani, Marco |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Parametricity versus the Universal ..."
Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
Publisher's Version
Article: popl18main-p46-p doi:10.1145/3158126
|
| |
Pavlogiannis, Andreas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Optimal Dyck Reachability ..."
Optimal Dyck Reachability for Data-Dependence and Alias Analysis
Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Publisher's Version
Artifacts Functional
Article: popl18main-p187-p doi:10.1145/3158118
Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..."
Data-Centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya
(Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
Publisher's Version
Article: popl18main-p88-p doi:10.1145/3158119
|
| |
Pellissier, Luc |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Polyadic Approximations, Fibrations ..."
Polyadic Approximations, Fibrations and Intersection Types
Damiano Mazza, Luc Pellissier, and Pierre Vial
(CNRS, France; University of Paris 13, France; University of Paris Diderot, France)
Publisher's Version
Article: popl18main-p265-p doi:10.1145/3158094
|
| |
Peña, Lucas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Foundations for Natural Proofs ..."
Foundations for Natural Proofs and Quantifier Instantiation
Christof Löding, P. Madhusudan, and Lucas Peña
(RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p99-p doi:10.1145/3158098
|
| |
Pereira, Fernando Magno Quintão |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..."
Inference of Static Semantics for Incomplete C Programs
Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil)
Publisher's Version
Artifacts Functional
Article: popl18main-p110-p doi:10.1145/3158117
|
| |
Peyton Jones, Simon |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..."
Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p2-p doi:10.1145/3158093
|
| |
Pierce, Benjamin C. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..."
Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p18-p doi:10.1145/3158089
Proc. ACM Program. Lang., vol. 2, issue POPL: "Generating Good Generators ..."
Generating Good Generators for Inductive Relations
Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce
(University of Pennsylvania, USA; Princeton University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p170-p doi:10.1145/3158133
|
| |
Piessens, Frank |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Parametricity versus the Universal ..."
Parametricity versus the Universal Type
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
Publisher's Version
Article: popl18main-p46-p doi:10.1145/3158126
|
| |
Piróg, Maciej |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..."
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Artifacts Functional
Article: popl18main-p160-p doi:10.1145/3158096
|
| |
Podelski, Andreas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..."
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p145-p doi:10.1145/3158114
|
| |
Polesiuk, Piotr |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..."
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Artifacts Functional
Article: popl18main-p160-p doi:10.1145/3158096
|
| |
Popescu, Andrei |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Safety and Conservativity ..."
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Ondřej Kunčar and Andrei Popescu
(TU Munich, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania)
Publisher's Version
Article: popl18main-p50-p doi:10.1145/3158112
|
| |
Pouchet, Louis-Noel |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..."
Analytical Modeling of Cache Behavior for Affine Programs
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan
(Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
Publisher's Version
Article: popl18main-p175-p doi:10.1145/3158120
|
| |
Pulte, Christopher |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..."
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p5-p doi:10.1145/3158107
|
| |
Püschel, Markus |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Practical Construction for ..."
A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version
Artifacts Functional
Article: popl18main-p251-p doi:10.1145/3158143
|
| |
Radiček, Ivan
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..."
Monadic Refinements for Relational Cost Analysis
Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger
(Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl18main-p94-p doi:10.1145/3158124
|
| |
Ramsay, Steven J. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Higher-Order Constrained Horn ..."
Higher-Order Constrained Horn Clauses for Verification
Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay
(University of Oxford, UK; University of Bristol, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p253-p doi:10.1145/3158099
|
| |
Rastogi, Aseem |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..."
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p134-p doi:10.1145/3158153
|
| |
Rémy, Didier |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Principled Approach to Ornamentation ..."
A Principled Approach to Ornamentation in ML
Thomas Williams and Didier Rémy
(Inria, France)
Publisher's Version
Artifacts Functional
Article: popl18main-p200-p doi:10.1145/3158109
|
| |
Reps, Thomas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..."
Non-linear Reasoning for Invariant Synthesis
Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps
(Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p201-p doi:10.1145/3158142
|
| |
Ribeiro, Rodrigo G. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..."
Inference of Static Semantics for Incomplete C Programs
Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil)
Publisher's Version
Artifacts Functional
Article: popl18main-p110-p doi:10.1145/3158117
|
| |
Riely, James |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Transactions in Relaxed Memory ..."
Transactions in Relaxed Memory Architectures
Brijesh Dongol, Radha Jagadeesan, and James Riely
(Brunel University London, UK; DePaul University, USA)
Publisher's Version
Article: popl18main-p154-p doi:10.1145/3158106
|
| |
Rinetzky, Noam |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..."
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p124-p doi:10.1145/3158136
|
| |
Rioux, Nick |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..."
Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible
William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed
(Northeastern University, USA; Ochanomizu University, Japan)
Publisher's Version
Article: popl18main-p51-p doi:10.1145/3158110
|
| |
Rompf, Tiark |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Collapsing Towers of Interpreters ..."
Collapsing Towers of Interpreters
Nada Amin and Tiark Rompf
(University of Cambridge, UK; Purdue University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p33-p doi:10.1145/3158140
|
| |
Rouvoet, Arjen |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Portland State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p277-p doi:10.1145/3158104
|
| |
Rümmer, Philipp |
Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..."
String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p266-p doi:10.1145/3158092
|
| |
Sadayappan, P.
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..."
Analytical Modeling of Cache Behavior for Affine Programs
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan
(Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
Publisher's Version
Article: popl18main-p175-p doi:10.1145/3158120
|
| |
Sagiv, Mooly |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..."
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p145-p doi:10.1145/3158114
Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..."
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p124-p doi:10.1145/3158136
|
| |
Sagonas, Konstantinos |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..."
Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis
(National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany)
Publisher's Version
Artifacts Functional
Article: popl18main-p80-p doi:10.1145/3158105
|
| |
Sarkar, Susmit |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..."
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p5-p doi:10.1145/3158107
|
| |
Satake, Yuki |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Relatively Complete Refinement ..."
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Hiroshi Unno, Yuki Satake, and Tachio Terauchi
(University of Tsukuba, Japan; Waseda University, Japan)
Publisher's Version
Article: popl18main-p256-p doi:10.1145/3158100
|
| |
Scherer, Gabriel |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..."
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek
(Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
Publisher's Version
Article: popl18main-p31-p doi:10.1145/3158137
|
| |
Ścibior, Adam |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Scott, Ryan G. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..."
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p1-p doi:10.1145/3158141
|
| |
Sergey, Ilya |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Programming and Proving with ..."
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, and Zachary Tatlock
(University College London, UK; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p115-p doi:10.1145/3158116
|
| |
Sewell, Peter |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..."
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell
(University of Cambridge, UK; ARM, UK; University of St. Andrews, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p5-p doi:10.1145/3158107
|
| |
Shaikhha, Amir |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..."
Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p285-p doi:10.1145/3158101
|
| |
Sharma, Rahul |
Proc. ACM Program. Lang., vol. 2, issue POPL: "On Automatically Proving the ..."
On Automatically Proving the Correctness of math.h Implementations
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India)
Publisher's Version
Article: popl18main-p43-p doi:10.1145/3158135
|
| |
Shasha, Dennis |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Go with the Flow: Compositional ..."
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, and Thomas Wies
(New York University, USA)
Publisher's Version
Article: popl18main-p190-p doi:10.1145/3158125
|
| |
Shoham, Sharon |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..."
Reducing Liveness to Safety in First-Order Logic
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p145-p doi:10.1145/3158114
|
| |
Sieczkowski, Filip |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..."
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Artifacts Functional
Article: popl18main-p160-p doi:10.1145/3158096
|
| |
Singh, Gagandeep |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Practical Construction for ..."
A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version
Artifacts Functional
Article: popl18main-p251-p doi:10.1145/3158143
|
| |
Singh, Rishabh |
Proc. ACM Program. Lang., vol. 2, issue POPL: "WebRelate: Integrating Web ..."
WebRelate: Integrating Web Data with Spreadsheets using Examples
Jeevana Priya Inala and Rishabh Singh
(Massachusetts Institute of Technology, USA; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p114-p doi:10.1145/3158090
Proc. ACM Program. Lang., vol. 2, issue POPL: "Program Synthesis using Abstraction ..."
Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig, and Rishabh Singh
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Article: popl18main-p20-p doi:10.1145/3158151
|
| |
Sinha, Nishant |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..."
Data-Centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya
(Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
Publisher's Version
Article: popl18main-p88-p doi:10.1145/3158119
|
| |
Spiwack, Arnaud |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..."
Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p2-p doi:10.1145/3158093
|
| |
Staton, Sam |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Stefanesco, Léo |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..."
A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal
(KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark)
Publisher's Version
Artifacts Functional
Article: popl18main-p27-p doi:10.1145/3158152
|
| |
Strub, Pierre-Yves |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..."
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France)
Publisher's Version
Artifacts Functional
Article: popl18main-p106-p doi:10.1145/3158145
|
| |
Stucki, Sandro |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..."
Simplicitly: Foundations and Applications of Implicit Function Types
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki
(EPFL, Switzerland; Northeastern University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p247-p doi:10.1145/3158130
|
| |
Swamy, Nikhil |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..."
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy
(Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p134-p doi:10.1145/3158153
|
| |
Ta, Quang-Trung
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..."
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Publisher's Version
Artifacts Functional
Article: popl18main-p281-p doi:10.1145/3158097
|
| |
Tasson, Christine |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Measurable Cones and Stable, ..."
Measurable Cones and Stable, Measurable Functions: A Model for Probabilistic Higher-Order Programming
Thomas Ehrhard, Michele Pagani, and Christine Tasson
(University of Paris Diderot, France; CNRS, France)
Publisher's Version
Article: popl18main-p165-p doi:10.1145/3158147
|
| |
Tatlock, Zachary |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Programming and Proving with ..."
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, and Zachary Tatlock
(University College London, UK; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p115-p doi:10.1145/3158116
|
| |
Terauchi, Tachio |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Relatively Complete Refinement ..."
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Hiroshi Unno, Yuki Satake, and Tachio Terauchi
(University of Tsukuba, Japan; Waseda University, Japan)
Publisher's Version
Article: popl18main-p256-p doi:10.1145/3158100
|
| |
Timany, Amin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..."
A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal
(KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark)
Publisher's Version
Artifacts Functional
Article: popl18main-p27-p doi:10.1145/3158152
|
| |
Tobin-Hochstadt, Sam |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..."
Soft Contract Verification for Higher-Order Stateful Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland, USA; Indiana University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p197-p doi:10.1145/3158139
|
| |
Tolmach, Andrew |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Portland State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p277-p doi:10.1145/3158104
|
| |
Tondwalkar, Anish |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..."
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p1-p doi:10.1145/3158141
|
| |
Torlak, Emina |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Symbolic Types for Lenient ..."
Symbolic Types for Lenient Symbolic Execution
Stephen Chang, Alex Knauth, and Emina Torlak
(Northeastern University, USA; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p180-p doi:10.1145/3158128
|
| |
Unno, Hiroshi
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Relatively Complete Refinement ..."
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
Hiroshi Unno, Yuki Satake, and Tachio Terauchi
(University of Tsukuba, Japan; Waseda University, Japan)
Publisher's Version
Article: popl18main-p256-p doi:10.1145/3158100
|
| |
Vafeiadis, Viktor
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..."
Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis
(National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany)
Publisher's Version
Artifacts Functional
Article: popl18main-p80-p doi:10.1145/3158105
|
| |
Vaidya, Kapil |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..."
Data-Centric Dynamic Partial Order Reduction
Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya
(Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
Publisher's Version
Article: popl18main-p88-p doi:10.1145/3158119
|
| |
Vákár, Matthijs |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Van Horn, David |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..."
Soft Contract Verification for Higher-Order Stateful Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland, USA; Indiana University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p197-p doi:10.1145/3158139
|
| |
Vazou, Niki |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..."
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p1-p doi:10.1145/3158141
|
| |
Vechev, Martin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Practical Construction for ..."
A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version
Artifacts Functional
Article: popl18main-p251-p doi:10.1145/3158143
|
| |
Vezzosi, Andrea |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Decidability of Conversion ..."
Decidability of Conversion for Type Theory in Type Theory
Andreas Abel, Joakim Öhman, and Andrea Vezzosi
(University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p128-p doi:10.1145/3158111
|
| |
Vial, Pierre |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Polyadic Approximations, Fibrations ..."
Polyadic Approximations, Fibrations and Intersection Types
Damiano Mazza, Luc Pellissier, and Pierre Vial
(CNRS, France; University of Paris 13, France; University of Paris Diderot, France)
Publisher's Version
Article: popl18main-p265-p doi:10.1145/3158094
|
| |
Visser, Eelco |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Portland State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p277-p doi:10.1145/3158104
|
| |
Vitek, Jan |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..."
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek
(Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
Publisher's Version
Article: popl18main-p31-p doi:10.1145/3158137
|
| |
Voizard, Antoine |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..."
Unifying Analytic and Statically-Typed Quasiquotes
Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch
(EPFL, Switzerland; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p285-p doi:10.1145/3158101
|
| |
Vojnar, Tomáš |
Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..."
String Constraints with Concatenation and Transducers Solved Efficiently
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar
(Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden)
Publisher's Version
Artifacts Functional
Article: popl18main-p266-p doi:10.1145/3158092
|
| |
Wadler, Philip
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..."
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala
(University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK)
Publisher's Version
Artifacts Functional
Article: popl18main-p1-p doi:10.1145/3158141
|
| |
Walker, David |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..."
Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p18-p doi:10.1145/3158089
|
| |
Walkingshaw, Eric |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..."
Migrating Gradual Types
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw
(University of Louisiana at Lafayette, USA; Oregon State University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p239-p doi:10.1145/3158103
|
| |
Wang, Xinyu |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Program Synthesis using Abstraction ..."
Program Synthesis using Abstraction Refinement
Xinyu Wang, Isil Dillig, and Rishabh Singh
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Article: popl18main-p20-p doi:10.1145/3158151
|
| |
Wang, Yuepeng |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..."
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version
Article: popl18main-p19-p doi:10.1145/3158144
|
| |
Wies, Thomas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Go with the Flow: Compositional ..."
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Siddharth Krishna, Dennis Shasha, and Thomas Wies
(New York University, USA)
Publisher's Version
Article: popl18main-p190-p doi:10.1145/3158125
|
| |
Wilcox, James R. |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Programming and Proving with ..."
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, and Zachary Tatlock
(University College London, UK; University of Washington, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p115-p doi:10.1145/3158116
|
| |
Williams, Thomas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "A Principled Approach to Ornamentation ..."
A Principled Approach to Ornamentation in ML
Thomas Williams and Didier Rémy
(Inria, France)
Publisher's Version
Artifacts Functional
Article: popl18main-p200-p doi:10.1145/3158109
|
| |
Wood, Thomas |
Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..."
JaVerT: JavaScript Verification Toolchain
José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Artifacts Functional
Article: popl18main-p276-p doi:10.1145/3158138
|
| |
Wu, Zhilin |
Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..."
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
(University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
Publisher's Version
Article: popl18main-p264-p doi:10.1145/3158091
|
| |
Yang, Hongseok
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..."
Denotational Validation of Higher-Order Bayesian Inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani
(University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
Publisher's Version
Article: popl18main-p234-p doi:10.1145/3158148
|
| |
Yee, Ming-Ho |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..."
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek
(Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
Publisher's Version
Article: popl18main-p31-p doi:10.1145/3158137
|
| |
Ying, Mingsheng |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Algorithmic Analysis of Termination ..."
Algorithmic Analysis of Termination Problems for Quantum Programs
Yangjia Li and Mingsheng Ying
(Institute of Software at Chinese Academy of Sciences, China; University of Technology Sydney, Australia; Tsinghua University, China)
Publisher's Version
Article: popl18main-p47-p doi:10.1145/3158123
|
| |
Zdancewic, Steve
|
Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..."
Synthesizing Bijective Lenses
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p18-p doi:10.1145/3158089
|
| |
Zohar, Yoni |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..."
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar
(Tel Aviv University, Israel; VMware, USA; Stanford University, USA)
Publisher's Version
Artifacts Functional
Article: popl18main-p124-p doi:10.1145/3158136
|
| |
Zuleger, Florian |
Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..."
Monadic Refinements for Relational Cost Analysis
Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger
(Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
Publisher's Version
Article: popl18main-p94-p doi:10.1145/3158124
|