


default search action
Proceedings 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