default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDProceedings of the ACM on Programming Languages, Volume 4
Volume 4, Number POPL, January 2020
- Davide Barbarossa
, Giulio Manzonetto:
Taylor subsumes Scott, Berry, Kahn and Plotkin. 1:1-1:23 - Martin Clochard, Claude Marché, Andrei Paskevich:
Deductive verification with ghost monitors. 2:1-2:26 - Stephen Chang, Michael Ballantyne, Milo Turner, William J. Bowman:
Dependent type systems as macros. 3:1-3:29 - Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder:
The next 700 relational program logics. 4:1-4:33 - Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Complexity and information in invariant inference. 5:1-5:29 - Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers:
Actris: session-type based reasoning in separation logic. 6:1-6:30 - Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu:
Formal verification of a constant-time preserving C compiler. 7:1-7:30 - Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter:
Coq Coq correct! verification of type checking and erasure for Coq, in Coq. 8:1-8:28 - Jason Z. S. Hu, Ondrej Lhoták:
Undecidability of d<: and its decidable fragments. 9:1-9:30 - Peter W. O'Hearn:
Incorrectness logic. 10:1-10:32 - Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis:
Persistency semantics of the Intel-x86 architecture. 11:1-11:31 - Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova:
Program synthesis by type-guided abstraction refinement. 12:1-12:28 - Azadeh Farzan, Anthony Vandikas:
Reductions for safety proofs. 13:1-13:28 - Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur:
Deterministic parallel fixpoint computation. 14:1-14:33 - G. A. Kavvos, Edward Morehouse, Daniel R. Licata, Norman Danner:
Recurrence extraction for functional programs through call-by-push-value. 15:1-15:31 - Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang:
Towards verified stochastic variational inference for probabilistic programs. 16:1-16:33 - Andreas Pavlogiannis:
Fast, sound, and effectively complete dynamic race prediction. 17:1-17:29 - Federico Aschieri, Francesco A. Genco:
Par means parallel: multiplicative linear logic proofs as concurrent functional programs. 18:1-18:28 - Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, Vikash K. Mansinghka:
Trace types and denotational semantics for sound programmable inference in probabilistic languages. 19:1-19:32 - Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon:
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. 20:1-20:31 - Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou:
Relational proofs for quantum programs. 21:1-21:29 - Michael Arntzenius, Neel Krishnaswami:
Seminaïve evaluation for a higher-order functional language. 22:1-22:28 - Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, Chung-Kil Hur:
CompCertM: CompCert with C-assembly linking and lightweight modular verification. 23:1-23:31 - Martin A. T. Handley, Niki Vazou, Graham Hutton:
Liquidate your assets: reasoning about resource usage in liquid Haskell. 24:1-24:27 - Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, Ming Xu:
Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. 25:1-25:30 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Rojin Rezvan:
Parameterized verification under TSO is PSPACE-complete. 26:1-26:29 - Yannick Forster, Fabian Kunze, Marc Roth:
The weak call-by-value λ-calculus is reasonable for both time and space. 27:1-27:23 - Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, Dusko Pavlovic:
Abstract extensionality: on the properties of incomplete abstract interpretations. 28:1-28:28 - Zeina Migeed, Jens Palsberg:
What is decidable about gradual types? 29:1-29:29 - David Binder, Julian Jabs, Ingo Skupin, Klaus Ostermann:
Decomposition diversity with symmetric data and codata. 30:1-30:28 - Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi:
Reduction monads and their signatures. 31:1-31:29 - Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak:
The high-level benefits of low-level sandboxing. 32:1-32:32 - Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan:
Spy game: verifying a local generic solver in Iris. 33:1-33:28 - Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer:
RustBelt meets relaxed memory. 34:1-34:29 - Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, Mahesh Viswanathan:
Deciding memory safety for single-pass heap-manipulating programs. 35:1-35:29 - Feras A. Saad, Cameron E. Freer, Martin C. Rinard, Vikash K. Mansinghka:
Optimal approximate sampling from discrete probability distributions. 36:1-36:31 - Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen:
Aiming low is harder: induction for lower bounds in probabilistic program verification. 37:1-37:28 - Martín Abadi, Gordon D. Plotkin:
A simple differentiable programming language. 38:1-38:28 - Alexander Vandenbroucke, Tom Schrijvers:
PλωNK: functional probabilistic NetKAT. 39:1-39:27 - Mark P. Jones, J. Garrett Morris, Richard A. Eisenberg:
Partial type constructors: or, making ad hoc datatypes less ad hoc. 40:1-40:28 - Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer:
Stacked borrows: an aliasing model for Rust. 41:1-41:32 - Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker:
Abstract interpretation of distributed network control planes. 42:1-42:27 - Michael Greenberg, Austin J. Blatt:
Executable formal semantics for the POSIX shell. 43:1-43:30 - Timothy Bourke, Lélio Brun, Marc Pouzet:
Mechanized semantics and verified compilation for a dataflow synchronous language with reset. 44:1-44:29 - Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs:
The future is ours: prophecy variables in separation logic. 45:1-45:32 - Max S. New, Dustin Jamner, Amal Ahmed:
Graduality and parametricity: together again for the first time. 46:1-46:32 - Sam Westrick, Rohan Yadav, Matthew Fluet, Umut A. Acar:
Disentanglement in nested-parallel programs. 47:1-47:32 - Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski:
Binders by day, labels by night: effect instances via lexically scoped handlers. 48:1-48:29 - Chenglong Wang, Yu Feng, Rastislav Bodík, Alvin Cheung, Isil Dillig:
Visualization by example. 49:1-49:28 - David Darais, Ian Sweet, Chang Liu, Michael Hicks:
A language for probabilistically oblivious computation. 50:1-50:31 - Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic:
Interaction trees: representing recursive and impure programs in Coq. 51:1-51:32 - Malavika Samak, Deokhwan Kim, Martin C. Rinard:
Synthesizing replacement classes. 52:1-52:33 - Ningning Xie, Richard A. Eisenberg, Bruno C. d. S. Oliveira:
Kind inference for datatypes. 53:1-53:28 - Suguman Bansal, Kedar S. Namjoshi, Yaniv Sa'ar:
Synthesis of coordination programs from linear temporal specifications. 54:1-54:27 - Gilles Barthe, Justin Hsu, Kevin Liao:
A probabilistic separation logic. 55:1-55:30 - Shengwei An, Rishabh Singh, Sasa Misailovic, Roopsha Samanta:
Augmented example-based synthesis using relational perturbation properties. 56:1-56:24 - Fredrik Dahlqvist, Dexter Kozen:
Semantics of higher-order probabilistic programs with conditioning. 57:1-57:29 - Pierre-Marie Pédrot, Nicolas Tabareau:
The fire triangle: how to mix substitution, dependent elimination, and effects. 58:1-58:28 - Guilhem Jaber:
SyTeCi: automating contextual equivalence for higher-order programs with references. 59:1-59:28 - Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, Zhendong Su:
Detecting floating-point errors via atomic conditions. 60:1-60:27 - Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, Alexandra Silva:
Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. 61:1-61:28 - Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, Bernhard Scholz:
Provenance-guided synthesis of Datalog programs. 62:1-62:27 - Pierre Clairambault, Marc de Visme:
Full abstraction for the quantum lambda-calculus. 63:1-63:28 - Aloïs Brunel, Damiano Mazza, Michele Pagani:
Backpropagation in the simply typed lambda-calculus with linear negation. 64:1-64:27 - Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, Christos Dimoulas:
Does blame shifting work? 65:1-65:29 - Julian Mackay, Alex Potanin, Jonathan Aldrich, Lindsay Groves:
Decidable subtyping for path dependent types. 66:1-66:27 - Peter Thiemann, Vasco T. Vasconcelos:
Label-dependent session types. 67:1-67:29 - Roland Meyer, Sebastian Wolff:
Pointer life cycle types for lock-free data structures with memory reclamation. 68:1-68:36
Volume 4, Number HOPL, June 2020
- Roger K. W. Hui, Morten Kromberg:
APL since 1978. 69:1-69:108 - Bjarne Stroustrup:
Thriving in a crowded and changing world: C++ 2006-2020. 70:1-70:168 - Rich Hickey:
A history of Clojure. 71:1-71:46 - John Reid, Bill Long, Jon Steidel:
History of coarrays and SPMD parallelism in Fortran. 72:1-72:30 - Walter Bright, Andrei Alexandrescu, Michael Parker:
Origins of the D programming language. 73:1-73:38 - Stefan Monnier, Michael Sperber:
Evolution of Emacs Lisp. 74:1-74:55 - Don Syme:
The early history of F#. 75:1-75:58 - Paul King:
A history of the Groovy programming language. 76:1-76:53 - Allen Wirfs-Brock, Brendan Eich:
JavaScript: the first 20 years. 77:1-77:189 - Jeffrey Kodosky:
LabVIEW. 78:1-78:54 - Cynthia Solomon, Brian Harvey, Ken Kahn, Henry Lieberman, Mark L. Miller, Margaret Minsky, Artemis Papert, Brian Silverman:
History of Logo. 79:1-79:66 - William D. Clinger, Mitchell Wand:
Hygienic macro technology. 80:1-80:110 - Cleve Moler, Jack Little:
A history of MATLAB. 81:1-81:67 - Brad J. Cox, Steve Naroff, Hansen Hsu:
The origins of Objective-C at PPI/Stepstone and its evolution at NeXT. 82:1-82:74 - Peter Van Roy, Seif Haridi, Christian Schulte, Gert Smolka:
A history of the Oz multiparadigm language. 83:1-83:56 - John M. Chambers:
S, R, and data science. 84:1-84:17 - Daniel Ingalls:
The evolution of Smalltalk: from Smalltalk-72 through Squeak. 85:1-85:101 - David MacQueen, Robert Harper, John H. Reppy:
The history of Standard ML. 86:1-86:100 - Peter Flake, Phil Moorby, Steve Golson, Arturo Salz, Simon J. Davidmann:
Verilog HDL and its ancestors and descendants. 87:1-87:90
Volume 4, Number ICFP, August 2020
- Xiaohong Chen, Grigore Rosu:
A general approach to define binders using matching logic. 88:1-88:32 - Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, Dimitrios Vytiniotis:
A quick look at impredicativity. 89:1-89:29 - Andreas Abel, Jean-Philippe Bernardy:
A unified view of modalities in type systems. 90:1-90:28 - Matus Tejiscak:
A dependently typed calculus with pattern matching and erasure inference. 91:1-91:29 - Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, Michel Steuwer:
Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies. 92:1-92:29 - Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann:
Compiling effect handlers in capability-passing style. 93:1-93:28 - Matthew Weidner, Heather Miller, Christopher Meiklejohn:
Composing and decomposing op-based CRDTs with semidirect products. 94:1-94:27 - Nick Rioux, Steve Zdancewic:
Computation focusing. 95:1-95:27 - Glen Mével, Jacques-Henri Jourdan, François Pottier:
Cosmo: a concurrent separation logic for multicore OCaml. 96:1-96:29 - Joseph W. Cutler, Daniel R. Licata, Norman Danner:
Denotational recurrence extraction for amortized analysis. 97:1-97:29 - Nándor Licker, Timothy M. Jones:
Duplo: a framework for OCaml post-link optimisation. 98:1-98:29 - Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, Daan Leijen:
Effect handlers, evidently. 99:1-99:29 - Daniel Hillerström, Sam Lindley, John Longley:
Effects for efficiency: asymptotic speedup with first-class control. 100:1-100:29 - András Kovács:
Elaboration with first-class implicit function types. 101:1-101:29 - Zachary Palmer, Theodore Park, Scott F. Smith, Shiwei Weng:
Higher-order demand-driven symbolic evaluation. 102:1-102:28 - Gabriel Radanne, Hannes Saffrich, Peter Thiemann:
Kindly bent to free us. 103:1-103:29 - Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg:
Kinds are calling conventions. 104:1-104:29 - Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama:
Liquid information flow control. 105:1-105:30 - Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, Nadia Polikarpova:
Liquid resource types. 106:1-106:29 - Sebastian Graf, Simon Peyton Jones, Ryan G. Scott:
Lower your guards: a compositional pattern-match coverage checker. 107:1-107:30 - Pierce Darragh, Michael D. Adams:
Parsing with zippers (functional pearl). 108:1-108:28 - Justin Lubin, Nick Collins, Cyrus Omar, Ravi Chugh:
Program sketching with live bidirectional evaluation. 109:1-109:29 - Di Wang, David M. Kahn, Jan Hoffmann:
Raising expectations: automating expected cost analysis with types. 110:1-110:31 - Vikraman Choudhury, Neel Krishnaswami:
Recovering purity with comonads and capabilities. 111:1-111:28 - Timothée Haudebourg, Thomas Genet, Thomas P. Jensen:
Regular language type inference with term rewriting. 112:1-112:29 - K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, Anil Madhavapeddy:
Retrofitting parallelism onto OCaml. 113:1-113:30 - Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers:
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. 114:1-114:29 - Daniel Selsam, Simon Hudon, Leonardo de Moura:
Sealing pointer-based optimizations behind pure functions. 115:1-115:20 - Arthur Charguéraud:
Separation logic for sequential programs (functional pearl). 116:1-116:34 - Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi:
Signature restriction for polymorphic algebraic effects. 117:1-117:30 - Kazutaka Matsuda, Meng Wang:
Sparcl: a language for partially-invertible computation. 118:1-118:31 - Benoît Montagu, Thomas P. Jensen:
Stable relations and abstract interpretation of higher-order programs. 119:1-119:30 - Jamie Willis, Nicolas Wu, Matthew Pickering:
Staged selective parser combinators. 120:1-120:30 - Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez:
SteelCore: an extensible concurrent separation logic for effectful dependently typed programs. 121:1-121:30 - Aaron Stump, Christopher Jenkins, Stephan Spahn, Colin McDonald:
Strong functional pearl: Harper's regular-expression matcher in Cedille. 122:1-122:25 - Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin:
TLC: temporal logic of distributed components. 123:1-123:30 - Lionel Parreaux:
The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl). 124:1-124:28
Volume 4, Number OOPSLA, November 2020
- Magnus Madsen, Ondrej Lhoták:
Fixpoints for the masses: programming with first-class Datalog constraints. 125:1-125:28 - Jonathan Immanuel Brachthäuser, Philipp Schuster, Klaus Ostermann:
Effects as capabilities: effect handlers and lightweight effect polymorphism. 126:1-126:30 - André Pacak, Sebastian Erdweg, Tamás Szabó:
A systematic approach to deriving incremental type checkers. 127:1-127:28 - Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham:
Proving highly-concurrent traversals correct. 128:1-128:29 - Cyril Six, Sylvain Boulmé, David Monniaux:
Certified and efficient instruction scheduling: application to interlocked VLIW processors. 129:1-129:29 - Giulia Meuli, Mathias Soeken, Martin Roetteler, Thomas Häner:
Enabling accuracy-aware Quantum compilers using symbolic resource estimation. 130:1-130:26 - Guilherme V. Leobas, Fernando Magno Quintão Pereira:
Semiring optimizations: dynamic elision of expressions with identity and absorbing elements. 131:1-131:28 - Michael J. Coblenz, Jonathan Aldrich, Brad A. Myers, Joshua Sunshine:
Can advanced type systems be usable? An empirical study of ownership, assets, and typestate in Obsidian. 132:1-132:28 - Thomas Häner, Torsten Hoefler, Matthias Troyer:
Assertion-based optimization of Quantum programs. 133:1-133:20 - Rupak Majumdar, Nobuko Yoshida, Damien Zufferey:
Multiparty motion coordination: from choreographies to robotics programs. 134:1-134:30 - Shankara Pailoor, Xinyu Wang, Hovav Shacham, Isil Dillig:
Automated policy synthesis for system call sandboxing. 135:1-135:26 - Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers:
How do programmers use unsafe rust? 136:1-136:27 - Yu Wang, Ke Wang, Fengjuan Gao, Linzhang Wang:
Learning semantic program embeddings with graph interval neural network. 137:1-137:27 - Breanna Devore-McDonald, Emery D. Berger:
Mossad: defeating software plagiarism detection. 138:1-138:28 - Yizhou Zhang, Guido Salvaneschi, Andrew C. Myers:
Handling bidirectional control flow. 139:1-139:30 - Steven Holtzen, Guy Van den Broeck, Todd D. Millstein:
Scaling exact inference for discrete probabilistic programs. 140:1-140:31 - Aaron Bembenek, Michael Greenberg, Stephen Chong:
Formulog: Datalog for SMT-based static analysis. 141:1-141:31 - Tongtong Xiang, Jeff Y. Luo, Werner Dietl:
Precise inference of expressive units of measurement types. 142:1-142:28 - Hongyu Liu, Sam Silvestro, Xiangyu Zhang, Jian Huang, Tongping Liu:
WATCHER: in-situ failure diagnosis. 143:1-143:27 - Thodoris Sotiropoulos, Stefanos Chaliasos, Dimitris Mitropoulos, Diomidis Spinellis:
A model for detecting faults in build specifications. 144:1-144:30 - Sean Bartell, Will Dietz, Vikram S. Adve:
Guided linking: dynamic linking without the costs. 145:1-145:29 - Hamed Gorjiara, Guoqing Harry Xu, Brian Demsky:
Satune: synthesizing efficient SAT encoders. 146:1-146:32 - Shengjian Guo, Yueqi Chen, Jiyong Yu, Meng Wu, Zhiqiang Zuo, Peng Li, Yueqiang Cheng, Huibo Wang:
Exposing cache timing side-channel leaks through out-of-order symbolic execution. 147:1-147:32 - Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, Nobuko Yoshida:
Statically verified refinements for multiparty protocols. 148:1-148:30 - Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, Nobuko Yoshida:
Featherweight go. 149:1-149:29 - Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, Yuan Xie:
Projection-based runtime assertions for testing and debugging Quantum programs. 150:1-150:29 - Azalea Raad, Ori Lahav, Viktor Vafeiadis:
Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. 151:1-151:28 - Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, David A. Basin:
Igloo: soundly linking compositional refinement and separation logic for distributed system verification. 152:1-152:31 - Konstantinos Kallas, Filip Niksic, Caleb Stanford, Rajeev Alur:
DiffStream: differential output testing for stream processing programs. 153:1-153:29 - Magnus Madsen, Jaco van de Pol:
Polymorphic types and effects with Boolean unification. 154:1-154:29 - David Castro-Perez, Nobuko Yoshida:
CAMP: cost-aware multiparty session protocols. 155:1-155:30 - Cormac Flanagan, Stephen N. Freund:
The anchor verifier for blocking and non-blocking concurrent software. 156:1-156:29 - Ramy Shahin, Marsha Chechik:
Automatic and efficient variability-aware lifting of functional programs. 157:1-157:27 - Ryan Senanayake, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen Chou, Shoaib Kamil, Saman P. Amarasinghe, Fredrik Kjolstad:
A sparse iteration space transformation framework for sparse tensor algebra. 158:1-158:30 - Hila Peleg, Roi Gabay, Shachar Itzhaky, Eran Yahav:
Programming with a read-eval-synth loop. 159:1-159:30 - Umar Farooq, Zhijia Zhao, Manu Sridharan, Iulian Neamtiu:
LiveDroid: identifying and preserving mobile app state in volatile runtime environments. 160:1-160:30 - Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Rosu:
Towards a unified proof framework for automated fixpoint reasoning using matching logic. 161:1-161:29 - Noam Yefet, Uri Alon, Eran Yahav:
Adversarial examples for models of code. 162:1-162:30 - Milijana Surbatovich, Brandon Lucia, Limin Jia:
Towards a formal foundation of intermittent computing. 163:1-163:31 - Guannan Wei, Oliver Bracevac, Shangyin Tan, Tiark Rompf:
Compiling symbolic execution with staging and algebraic effects. 164:1-164:33 - Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, Aaron Roth:
Testing differential privacy with dual interpreters. 165:1-165:26 - Julie L. Newcomb, Andrew Adams, Steven Johnson, Rastislav Bodík, Shoaib Kamil:
Verifying and improving Halide's term rewriting system with program synthesis. 166:1-166:28 - Gabriel Poesia, Fernando Magno Quintão Pereira:
Dynamic dispatch of context-sensitive optimizations. 167:1-167:28 - Anders Møller, Oskar Haarklou Veileborg:
Eliminating abstraction overhead of Java stream pipelines using ahead-of-time program optimization. 168:1-168:29 - Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt:
Build scripts with perfect dependencies. 169:1-169:28 - John K. Feser, Sam Madden, Nan Tang, Armando Solar-Lezama:
Deductive optimization of relational data storage. 170:1-170:30 - Joshua Clune, Vijay Ramamurthy, Ruben Martins, Umut A. Acar:
Program equivalence for assisted grading of functional programs. 171:1-171:29 - Martin Avanzini, Georg Moser, Michael Schaper:
A modular cost analysis for probabilistic programs. 172:1-172:30 - Dietrich Geisler, Irene Yoon, Aditi Kabra, Horace He, Yinnon Sanders, Adrian Sampson:
Geometry types for graphics programming. 173:1-173:25 - Zhefeng Wu, Zhe Sun, Kai Gong, Lingyun Chen, Bin Liao, Yihua Jin:
Hidden inheritance: an inline caching design for TypeScript performance. 174:1-174:29 - Fengyun Liu, Ondrej Lhoták, Aggelos Biboudis, Paolo G. Giarrusso, Martin Odersky:
A type-and-effect system for object initialization. 175:1-175:28 - Subarno Banerjee, David Devecsery, Peter M. Chen, Satish Narayanasamy:
Sound garbage collection for C using pointer provenance. 176:1-176:28 - Manasij Mukherjee, Pranav Kant, Zhengyang Liu, John Regehr:
Dataflow-based pruning for speeding up superoptimization. 177:1-177:24 - Ana L. Milanova:
FlowCFL: generalized type-based reachability analysis: graph reduction and equivalence of CFL-based and type-based reachability. 178:1-178:29 - Minseok Jeon, Myungho Lee, Hakjoo Oh:
Learning graph-based heuristics for pointer analysis without handcrafting application-specific features. 179:1-179:30 - Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser:
Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications. 180:1-180:28 - Alexi Turcotte, Aviral Goel, Filip Krikava, Jan Vitek:
Designing types for R, empirically. 181:1-181:25 - Aayan Kumar, Vivek Seshadri, Rahul Sharma:
Shiftry: RNN inference in 2KB of RAM. 182:1-182:30 - Lingkun Kong, Konstantinos Mamouras:
StreamQL: a query language for processing streaming time series. 183:1-183:32 - Qianshan Yu, Fei He, Bow-Yaw Wang:
Incremental predicate analysis for regression verification. 184:1-184:25 - Caterina Urban, Maria Christakis, Valentin Wüstholz, Fuyuan Zhang:
Perfectly parallel fairness certification of neural networks. 185:1-185:30 - Quentin Stiévenart, Magnus Madsen:
Fuzzing channel-based concurrency runtimes using types and effects. 186:1-186:27 - Anders Møller, Benjamin Barslev Nielsen, Martin Toldam Torp:
Detecting locations in JavaScript programs affected by breaking library changes. 187:1-187:25 - Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, Guido Salvaneschi:
Rethinking safe consistency in distributed object-oriented programming. 188:1-188:30 - Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, ThanhVu Nguyen:
DynamiTe: dynamic termination and non-termination proofs. 189:1-189:30 - Sifis Lagouvardos, Neville Grech, Ilias Tsatiris, Yannis Smaragdakis:
Precise static modeling of Ethereum "memory". 190:1-190:26 - John Peter Campora III, Sheng Chen:
Taming type annotations in gradual typing. 191:1-191:30 - Minh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar:
Inter-theory dependency analysis for SMT string solvers. 192:1-192:27 - Dominik Winterer, Chengyu Zhang, Zhendong Su:
On the unusual effectiveness of type-aware operator mutations for testing SMT solvers. 193:1-193:25 - Radha Jagadeesan, Alan Jeffrey, James Riely:
Pomsets with preconditions: a simple model of relaxed memory. 194:1-194:30 - Tobias Grosser, Theodoros Theodoridis, Maximilian Falkenstein, Arjun Pitchanathan, Michael Kruse, Manuel Rigger, Zhendong Su, Torsten Hoefler:
Fast linear programming through transprecision computing on small and sparse data. 195:1-195:28 - Vsevolod Livinskii, Dmitry Babokin, John Regehr:
Random testing for C and C++ compilers with YARPGen. 196:1-196:25 - Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao:
CompCertELF: verified separate compilation of C programs into ELF object files. 197:1-197:28 - Bo Sang, Patrick Eugster, Gustavo Petri, Srivatsan Ravi, Pierre-Louis Roman:
Scalable and serializable networked multi-actor programming. 198:1-198:30 - Fei He, Jitao Han:
Termination analysis for evolving programs: an incremental approach by reusing certified modules. 199:1-199:27 - Eric Atkinson, Michael Carbin:
Programming and reasoning with partial observability. 200:1-200:28 - Ivan Gavran, Eva Darulova, Rupak Majumdar:
Interactive synthesis of temporal specifications from examples and natural language. 201:1-201:26 - Wing Lam, Stefan Winter, Anjiang Wei, Tao Xie, Darko Marinov, Jonathan Bell:
A large-scale longitudinal study of flaky tests. 202:1-202:29 - Hailong Zhang, Yu Hao, Sufian Latif, Raef Bassily, Atanas Rountev:
Differentially-private software frequency profiling under linear constraints. 203:1-203:24 - Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan:
Do you have space for dessert? a verified space cost semantics for CakeML programs. 204:1-204:29 - Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova:
Digging for fold: synthesis-aided API discovery for Haskell. 205:1-205:27 - Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, Georgios Karachalias:
Resolution as intersection subtyping via Modus Ponens. 206:1-206:30 - Julia Belyakova, Benjamin Chung, Jack Gelinas, Jameson Nash, Ross Tate, Jan Vitek:
World age in Julia: optimizing method dispatch in the presence of eval. 207:1-207:26 - Ifaz Kabir, Yufeng Li, Ondrej Lhoták:
ιDOT: a DOT calculus with object initialization. 208:1-208:28 - Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv:
Taming callbacks for smart contract modularity. 209:1-209:30 - Cezara Dragoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic:
Testing consensus implementations using communication closure. 210:1-210:29 - Manuel Rigger, Zhendong Su:
Finding bugs in database systems via query partitioning. 211:1-211:30 - Sumit Gulwani, Vu Le, Arjun Radhakrishna, Ivan Radicek, Mohammad Raza:
Structure interpretation of text formats. 212:1-212:29 - Cezara Dragoi, Josef Widder, Damien Zufferey:
Programming at the edge of synchrony. 213:1-213:30 - Mehdi Bagherzadeh, Nicholas Fireman, Anas Shawesh, Raffi Khatchadourian:
Actor concurrency bugs: a comprehensive study on symptoms, root causes, API usages, and differences. 214:1-214:32 - Shaked Brody, Uri Alon, Eran Yahav:
A structural model for contextual code changes. 215:1-215:28 - Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou:
Verifying replicated data types with typeclass refinements in Liquid Haskell. 216:1-216:30 - Pengyu Nie, Marinela Parovic, Zhiqiang Zang, Sarfraz Khurshid, Aleksandar Milicevic, Milos Gligoric:
Unifying execution of imperative generators and declarative specifications. 217:1-217:26 - Lenka Turonová, Lukás Holík, Ondrej Lengál, Olli Saarikivi, Margus Veanes, Tomás Vojnar:
Regex matching with counting-set automata. 218:1-218:30 - Xiang Gao, Shraddha Barke, Arjun Radhakrishna, Gustavo Soares, Sumit Gulwani, Alan Leung, Nachiappan Nagappan, Ashish Tiwari:
Feedback-driven semi-supervised synthesis of program transformations. 219:1-219:30 - Olivier Flückiger, Guido Chari, Ming-Ho Yee, Jan Jecmen, Jakob Hain, Jan Vitek:
Contextual dispatch for function specialization. 220:1-220:24 - Shubhani Gupta, Abhishek Rose, Sorav Bansal:
Counterexample-guided correlation algorithm for translation validation. 221:1-221:29 - Leif Andersen, Michael Ballantyne, Matthias Felleisen:
Adding interactive visual syntax to textual code. 222:1-222:28 - Yaoda Zhou, Bruno C. d. S. Oliveira, Jinxu Zhao:
Revisiting iso-recursive subtyping. 223:1-223:28 - Ruyi Ji, Yican Sun, Yingfei Xiong, Zhenjiang Hu:
Guiding dynamic programing via structural probability for accelerating programming by example. 224:1-224:29 - Yaniv David, Uri Alon, Eran Yahav:
Neural reverse engineering of stripped binaries using augmented control flow graphs. 225:1-225:28 - Jake Kirkham, Tyler Sorensen, Esin Tureci, Margaret Martonosi:
Foundations of empirical memory consistency testing. 226:1-226:29 - Shraddha Barke, Hila Peleg, Nadia Polikarpova:
Just-in-time learning for bottom-up enumerative synthesis. 227:1-227:29 - Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, Joshua Sunshine:
Gradual verification of recursive heap data structures. 228:1-228:28 - Michael Ballantyne, Alexis King, Matthias Felleisen:
Macros for domain-specific languages. 229:1-229:29 - Suvam Mukherjee, Pantazis Deligiannis, Arpita Biswas, Akash Lal:
Learning-based controlled concurrency testing. 230:1-230:31 - Emily First, Yuriy Brun, Arjun Guha:
TacTok: semantics-aware proof synthesis. 231:1-231:31 - Ritwika Ghosh, Chiao Hsieh, Sasa Misailovic, Sayan Mitra:
Koord: a language for programming and verifying distributed robotics application. 232:1-232:30 - Yulei Sui, Xiao Cheng, Guanqin Zhang, Haoyu Wang:
Flow2Vec: value-flow-based precise code embedding. 233:1-233:27
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-08 22:11 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
