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