Proceedings of the ACM on Programming Languages 2019: all accepted papers
- code2vec: learning distributed representations of code ↗Uri Alon, Meital Zilberstein, Omer Levy et al.1,215 citations
- An abstract domain for certifying neural networks ↗Gagandeep Singh, Timon Gehr, Markus Püschel et al.609 citations
- Getafix: learning to fix bugs automaticallyJohannes Bader, Andrew Scott, Michael Pradel et al.227 citations · our summary
- Improving bug detection via context-based code representation learning and attention-based neural networks ↗Yi Li, Shaohua Wang, Tien N. Nguyen et al.162 citations
- Leveraging rust types for modular specification and verification ↗Vytautas Astrauskas, Péter Müller, Federico Poli et al.137 citations
- Interaction trees: representing recursive and impure programs in Coq ↗Li-yao Xia, Yannick Zakowski, Paul He et al.134 citations
- ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS ↗Alasdair Armstrong, Thomas Bauereiß, B. K. Campbell et al.132 citations
- Incorrectness logic ↗Peter W. O’Hearn122 citations
- Aroma: code recommendation via structural code search ↗Sifei Luan, Di Yang, Celeste Barnaby et al.104 citations
- Less is more: multiparty session types revisited ↗Alceste Scalas, Nobuko Yoshida102 citations
- Formal foundations of serverless computing ↗Abhinav Jangda, Donald Pinckney, Yuriy Brun et al.100 citations
- Safer smart contract programming with Scilla ↗Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen et al.94 citations
- Detecting nondeterministic payment bugs in Ethereum smart contracts ↗Shuai Wang, Chengyu Zhang, Zhendong Su84 citations
- Quantitative program reasoning with graded modal types ↗Dominic A. Orchard, Vilem-Benjamin Liepelt, Harley Eades84 citations
- Decision procedures for path feasibility of string-manipulating programs with complex operations ↗Taolue Chen, Matthew Hague, Anthony W. Lin et al.82 citations
- Formal verification of a constant-time preserving C compiler ↗Gilles Barthe, Sandrine Blazy, Benjamin Grégoire et al.77 citations
- Initialize once, start fast: application initialization at build time ↗Christian L. Wimmer, Codruţ Stancu, Peter Höfer et al.74 citations
- AutoPandas: neural-backed generators for program synthesis ↗Rohan Bavishi, Caroline Lemieux, Roy Fox et al.73 citations
- FuzzFactory: domain-specific fuzzing with waypoints ↗Rohan Padhye, Caroline Lemieux, Koushik Sen et al.73 citations
- Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems ↗Johannes Späth, Karim Ali, Eric Bodden72 citations
- Cubical agda: a dependently typed programming language with univalence and higher inductive types ↗Andrea Vezzosi, Anders Mörtberg, Andreas M. Abel71 citations
- Live functional programming with typed holes ↗Cyrus Omar, Ian Voysey, Ravi Chugh et al.68 citations
- Qubit allocation as a combination of subgraph isomorphism and token swapping ↗Marcos Yukio Siraichi, Vinícius Fernandes dos Santos, Caroline Collange et al.67 citations
- Stacked borrows: an aliasing model for Rust ↗Ralf Jung, Hoang-Hai Dang, Jeehoon Kang et al.67 citations
- Coq Coq correct! verification of type checking and erasure for Coq, in Coq ↗Matthieu Sozeau, Simon Boulier, Yannick Forster et al.66 citations
- RustBelt meets relaxed memory ↗Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser et al.65 citations
- CT-wasm: type-driven secure cryptography for the web ecosystem ↗Conrad Watt, John Renner, Natalie Popescu et al.63 citations
- Dijkstra monads for all ↗Kenji Maillard, Danel Ahman, Robert Atkey et al.62 citations
- Persistency semantics of the Intel-x86 architecture ↗Azalea Raad, John Wickerson, Gil Neiger et al.61 citations
- The future is ours: prophecy variables in separation logic ↗Ralf Jung, Rodolphe Lepigre, G. Parthasarathy et al.61 citations
- Grounding thin-air reads with event structures ↗Soham Chakraborty, Viktor Vafeiadis60 citations
- Demystifying differentiable programming: shift/reset the penultimate backpropagator ↗Fei Wang, Daniel Zheng, James Decker et al.59 citations
- IntelliMerge: a refactoring-aware software merging technique ↗Bo Shen, Wei Zhang, Haiyan Zhao et al.59 citations
- Pretend synchrony: synchronous verification of asynchronous distributed programs ↗Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst et al.58 citations
- Quantum relational Hoare logic ↗Dominique Unruh58 citations
- Probabilistic verification of fairness properties via concentration ↗Osbert Bastani, Xin Zhang, Armando Solar-Lezama57 citations
- Bridging the gap between programming languages and hardware weak memory models ↗Anton Podkopaev, Ori Lahav, Viktor Vafeiadis56 citations
- Definitional proof-irrelevance without K ↗Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau et al.55 citations
- Efficient lock-free durable sets ↗Yoav Zuriel, Michal Friedman, Gali Sheffi et al.55 citations
- Exploring C semantics and pointer provenance ↗Kayvan Memarian, Victor B. F. Gomes, Brooks Davis et al.55 citations
- Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures ↗David Castro, Raymond Hu, Sung-Shik Jongmans et al.54 citations
- On the complexity of checking transactional consistency ↗Ranadeep Biswas, Constantin Enea52 citations
- TLA+ model checking made symbolic ↗Igor Konnov, Jure Kukovec, Thanh-Hai Tran52 citations
- Diagrammatic algebra: from linear to concurrent systems ↗Filippo Bonchi, Joshua Holland, Robin Piedeleu et al.50 citations
- Exceptional asynchronous session types: session types without tiers ↗Simon Fowler, Sam Lindley, J. Garrett Morris et al.50 citations
- Provenance-guided synthesis of Datalog programs ↗Mukund Raghothaman, Jonathan Mendelson, David Zhao et al.50 citations
- A simple differentiable programming language ↗Martı́n Abadi, Gordon D. Plotkin49 citations
- CompCertM: CompCert with C-assembly linking and lightweight modular verification ↗Youngju Song, Minki Cho, Dongjoo Kim et al.49 citations
- Efficient automated repair of high floating-point errors in numerical libraries ↗Xin Yi, Liqian Chen, Xiaoguang Mao et al.49 citations
- Optimal stateless model checking for reads-from equivalence under sequential consistency ↗Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jönsson et al.49 citations
- An abstract stack based approach to verified compositional compilation to machine code ↗Yuting Wang, Pierre Wilke, Zhong Shao48 citations
- Efficient differentiable programming in a functional array-processing language ↗Amir Shaikhha, Andrew W Fitzgibbon, Dimitrios Vytiniotis et al.48 citations
- Structuring the synthesis of heap-manipulating programs ↗Nadia Polikarpova, Ilya Sergey48 citations
- Coverage guided, property based testing ↗Leonidas Lampropoulos, Michael Hicks, Benjamin C. Pierce47 citations
- Fast, sound, and effectively complete dynamic race prediction ↗Andreas Pavlogiannis47 citations
- On the fly synthesis of edit suggestions ↗Anders Miltner, Sumit Gulwani, Vu Le et al.47 citations
- Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models ↗Azalea Raad, John Wickerson, Viktor Vafeiadis47 citations
- Binders by day, labels by night: effect instances via lexically scoped handlers ↗Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk et al.46 citations
- Equations reloaded: high-level dependently-typed functional programming and proving in Coq ↗Matthieu Sozeau, Cyprien Mangin46 citations
- Precision-preserving yet fast object-sensitive pointer analysis with partial context sensitivity ↗Jingbo Lu, Jingling Xue46 citations
- Abstract interpretation of distributed network control planes ↗Ryan Beckett, Aarti Gupta, Ratul Mahajan et al.45 citations
- Abstraction-safe effect handlers via tunneling ↗Yizhou Zhang, Andrew C. Myers45 citations
- Aiming low is harder: induction for lower bounds in probabilistic program verification ↗Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl et al.45 citations
- Detecting floating-point errors via atomic conditions ↗Daming Zou, Muhan Zeng, Yingfei Xiong et al.45 citations
- Constructing quotient inductive-inductive types ↗Ambrus Kaposi, András Kovács, Thorsten Altenkirch44 citations
- Gradual typing: a new perspective ↗Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani et al.44 citations
- Program synthesis by type-guided abstraction refinement ↗Zheng Kui Guo, Michael B. James, David Justo et al.43 citations
- Quantitative separation logic: a logic for reasoning about probabilistic pointer programs ↗Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen et al.43 citations
- StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities ↗Lau Skorstengaard, Dominique Devriese, Lars Birkedal43 citations
- Actris: session-type based reasoning in separation logic ↗Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers42 citations
- Hamsaz: replication coordination analysis and synthesis ↗Farzin Houshmand, Mohsen Lesani42 citations
- A domain theory for statistical probabilistic programming ↗Matthijs Vákár, Ohad Kammar, Sam Staton41 citations
- Adventures in monitorability: from branching to linear time and back again ↗Luca Aceto, Antonis Achilleos, Adrian Francalanza et al.41 citations
- Compiler fuzzing: how much does it matter? ↗Michaël Marcozzi, Qiyi Tang, Alastair F. Donaldson et al.41 citations
- The fire triangle: how to mix substitution, dependent elimination, and effects ↗Pierre-Marie Pédrot, Nicolas Tabareau41 citations
- The next 700 relational program logics ↗Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas et al.41 citations
- A verified, efficient embedding of a verifiable assembly language ↗Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel et al.40 citations
- Modular verification for almost-sure termination of probabilistic programs ↗Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee et al.40 citations
- Bounded model checking of signal temporal logic properties using syntactic separation ↗Kyungmin Bae, Jia Lee39 citations
- On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models ↗Azalea Raad, Marko Doko, Lovro Rožić et al.38 citations
- A separation logic for concurrent randomized programs ↗Joseph Tassarotti, Robert Harper37 citations
- Liquidate your assets: reasoning about resource usage in liquid Haskell ↗Martin A. T. Handley, Niki Vazou, Graham Hutton37 citations
- Visualization by example ↗Chenglong Wang, Yu Feng, Rastislav Bodík et al.37 citations
- FrAngel: component-based synthesis with control structures ↗Kensen Shi, Jacob Steinhardt, Percy Liang36 citations
- Graduality and parametricity: together again for the first time ↗Max S. New, Dustin Jamner, Amal Ahmed36 citations
- The next 700 compiler correctness theorems (functional pearl) ↗DANIEL C. PATTERSON, Amal Ahmed36 citations
- A probabilistic separation logic ↗Gilles Barthe, Justin Hsu, Kevin Liao35 citations
- Reflection-aware static regression test selection ↗August Shi, Milica Hadzi-Tanovic, Lingming Zhang et al.35 citations
- Better late than never: a fully-abstract semantics for classical processes ↗Wen Kokke, Fabrizio Montesi, Marco Peressotti34 citations
- Automatic repair of regular expressions ↗Rong Pan, Qinheping Hu, Gaowei Xu et al.33 citations
- Closed forms for numerical loops ↗Zachary Kincaid, Jason Breck, John Cyphert et al.33 citations
- Implementing a modal dependent type theory ↗Daniel Gratzer, Jonathan Sterling, Lars Birkedal33 citations
- Mergeable replicated data types ↗Gowtham Kaki, Swarn Priya, KC Sivaramakrishnan et al.33 citations
- Semantics of higher-order probabilistic programs with conditioning ↗Fredrik Dahlqvist, Dexter C. Kozen33 citations
- Abstracting extensible data types: or, rows by any other name ↗J. Garrett Morris, James McKinna32 citations
- Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy ↗Joseph P. Near, David Darais, Chiké Abuah et al.32 citations
- Abstracting algebraic effects ↗Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk et al.31 citations
- Fast and exact analysis for LRU caches ↗Valentin Touzeau, Claire Maïza, David P. Monniaux et al.31 citations
- Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time ↗Steffen Smolka, Nate Foster, Justin Hsu et al.31 citations
- Higher inductive types in cubical computational type theory ↗Evan Cavallo, Robert W. Harper31 citations
This page in Markdown → https://md.research.elamur.ai/free/en/venues/proceedings-of-the-acm-on-programming-languages/2019/papers/