default search action
Proceedings of the ACM on Programming Languages, Volume 5
Volume 5, Number POPL, January 2021
- Denis Kuperberg
, Laureline Pinault, Damien Pous
Cyclic proofs, system t, and the power of contraction. 1-28 - Patrick Bahr, Christian Uldal Graulund, Rasmus Ejlers Møgelberg:
Diamonds are not forever: liveness in reactive programming with guarded recursion. 1-28 - Benjamin Sherman, Jesse Michel, Michael Carbin:
𝜆ₛ: computable semantics for differentiable programming with higher-order functions and datatypes. 1-31 - Roy Margalit
Verifying observational robustness against a c11-style memory model. 1-33 - Frantisek Farka
On algebraic abstractions for concurrent separation logics. 1-32 - Aïna Linn Georges
Efficient and provable local capability revocation using uninitialized capabilities. 1-30 - Koen Jacobs
Fully abstract from static to gradual. 1-30 - Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan:
Deciding accuracy of differential privacy schemes. 1-30 - Chao-Hong Chen
A computational interpretation of compact closed categories: reversible programming with negative and fractional types. 1-29 - Simon Oddershede Gregersen
Mechanized logical relations for termination-insensitive noninterference. 1-29 - Marcin Sabok, Sam Staton, Dario Stein, Michael Wolman:
Probabilistic programming semantics for name generation. 1-29 - Carlo Angiuli
Internalizing representation independence with univalence. 1-30 - Simon Spies, Neel Krishnaswami, Derek Dreyer:
Transfinite step-indexing for termination. 1-29 - Michael Benedikt, Cécilia Pradic:
Generating collection transformations from proofs. 1-28 - Yotam M. Y. Feldman
Learning the boundary of inductive invariants. 1-30 - Silvia Ghilezan
Precise subtyping for asynchronous multiparty sessions. 1-28 - Kostas Ferles, Jon Stephens, Isil Dillig:
Verifying correct usage of context-free API protocols. 1-30 - Jatin Arora
Provably space-efficient parallel functional programming. 1-33 - Zvonimir Pavlinovic, Yusen Su, Thomas Wies:
Data flow refinement type inference. 1-31 - Cambridge Yang, Eric Atkinson, Michael Carbin:
Simplifying dependent reductions in the polyhedral model. 1-33 - Marco Patrignani
On the semantic expressiveness of recursive types. 1-29 - Arjen Rouvoet, Robbert Krebbers, Eelco Visser:
Intrinsically typed compilation with nameless labels. 1-28 - Max Willsey
egg: Fast and extensible equality saturation. 1-29 - Danel Ahman
Asynchronous effects. 1-28 - Stefan K. Muller, Jan Hoffmann:
Modeling and analyzing evaluation cost of CUDA kernels. 1-31 - Lucas Silver, Steve Zdancewic:
Dijkstra monads forever: termination-sensitive specifications for interaction trees. 1-28 - Vineet Rajani
A unifying type-theory for higher-order (amortized) cost analysis. 1-28 - Damiano Mazza, Michele Pagani
Automatic differentiation in PCF. 1-27 - Jay P. Lim
An approach to generate correctly rounded math libraries for new floating point variants. 1-30 - Jinwoo Kim
Semantics-guided synthesis. 1-32 - Julian Rosemann, Simon Moll, Sebastian Hack:
An abstract interpretation for SPMD divergence on reducible control flow graphs. 1-31 - Ugo Dal Lago
Intersection types and (positive) almost-sure termination. 1-32 - Paulo Emílio de Vilhena, François Pottier:
A separation logic for effect handlers. 1-28 - Anders Alnor Mathiasen, Andreas Pavlogiannis
The fine-grained and parallel complexity of andersen's pointer analysis. 1-29 - Andrew K. Hirsch
Giving semantics to program-counter labels via secure effects. 1-29 - Umang Mathur
Optimal prediction of synchronization-preserving races. 1-29 - Kesha Hietala
A verified optimizer for Quantum circuits. 1-29 - Jens Oliver Gutsfeld, Markus Müller-Olm, Christoph Ohrem
Automata and fixpoints for asynchronous hyperproperties. 1-29 - Kevin Batz
Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. 1-30 - Nathanaël Courant
Verified code generation for the polyhedral model. 1-24 - Ryan Doenges
Petr4: formal foundations for p4 data planes. 1-32 - Léon Gondelman, Simon Oddershede Gregersen
Distributed causal memory: modular specification and verification in higher-order distributed separation logic. 1-29 - Michalis Kokologiannakis
PerSeVerE: persistency semantics for verification under ext4. 1-29 - Pascal Baumann
Context-bounded verification of liveness properties for multithreaded shared-memory programs. 1-31 - Alban Reynaud, Gabriel Scherer
A practical mode system for recursive definitions. 1-29 - Aurèle Barrière
Formally verified speculation and deoptimization in a JIT compiler. 1-26 - Artem Khyzha, Ori Lahav
Taming x86-TSO persistency. 1-29 - Shaull Almagor
Deciding ω-regular properties on linear recurrence sequences. 1-24 - Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Ranjit Jhala, Dean M. Tullsen
Automatically eliminating speculative leaks from cryptographic code with blade. 1-30 - Pritam Choudhury, Harley Eades III, Richard A. Eisenberg
A graded dependent type system with a usage-aware semantics. 1-32 - Beniamino Accattoli, Ugo Dal Lago
The (In)Efficiency of interaction. 1-33 - Alejandro Aguirre
A pre-expectation calculus for probabilistic sensitivity. 1-28 - Cameron Moy
Corpse reviver: sound and efficient gradual typing via contract verification. 1-28 - Woosuk Lee:
Combining the top-down propagation and bottom-up enumeration for inductive program synthesis. 1-28 - Eddie Jones
Intensional datatype refinement: with application to scalable verification of pattern-match safety. 1-29 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
Deciding reachability under persistent x86-TSO. 1-32 - Ivan Di Liberti
Functorial semantics for partial theories. 1-28 - Jules Jacobs
Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities. 1-26 - Yuanbo Li, Qirun Zhang
On the complexity of bidirected interleaved Dyck-reachability. 1-28 - Jesper Cockx, Nicolas Tabareau
The taming of the rew: a type theory with computational assumptions. 1-29 - Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, Ronald Garcia:
Abstracting gradual typing moving forward: precise and space-efficient. 1-28
Volume 5, Number ICFP, August 2021
- Shivam Handa, Konstantinos Kallas, Nikos Vasilakis, Martin C. Rinard:
An order-aware dataflow model for parallel Unix pipelines. 1-28 - Adam Paszke, Daniel D. Johnson, David Duvenaud, Dimitrios Vytiniotis, Alexey Radul, Matthew J. Johnson, Jonathan Ragan-Kelley, Dougal Maclaurin:
Getting to the point: index sets and parallelism-preserving autodiff for pointful array programming. 1-29 - Manuel Serrano
Of JavaScript AOT compilation performance. 1-30 - Ningning Xie, Daan Leijen:
Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C. 1-30 - Conal Elliott
Symbolic and automatic differentiation of languages. 1-18 - Donnacha Oisín Kidney
Algebras for weighted search. 1-30 - Zhixuan Yang
Reasoning about effect interaction by fusion. 1-29 - Zoe Paraskevopoulou, John M. Li, Andrew W. Appel
Compositional optimizations for CertiCoq. 1-30 - Nikita Zyuzin
Contextual modal types for algebraic effects and handlers. 1-29 - Alejandro Aguirre
Higher-order probabilistic adversarial computations: categorical semantics and program logics. 1-30 - Kimball Germane
Newly-single and loving it: improving higher-order must-alias analysis with heap fragments. 1-28 - Chaitanya Koparkar, Mike Rainey, Michael Vollmer, Milind Kulkarni
Efficient tree-traversals: reconciling parallelism and dense data representations. 1-29 - Glen Mével
Formal verification of a concurrent bounded queue in a weak memory model. 1-29 - Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux
Steel: proof-oriented programming in a dependently typed concurrent separation logic. 1-30 - Sandro Stucki
A theory of higher-order subtyping with type intervals. 1-30 - Pedro Rocha, Luís Caires
Propositions-as-types and shared state. 1-30 - Lars Birkedal
Theorems for free from separation logic specifications. 1-29 - Yannick Zakowski
Modular, compositional, and executable formal semantics for LLVM IR. 1-30 - Denis Merigoux
Catala: a programming language for the law. 1-29 - Nicolas Krauter
Persistent software transactional memory in Haskell. 1-29 - Taro Sekiyama
CPS transformation with affine types for call-by-value implicit polymorphism. 1-30 - Nick Giannarakis, Alexandra Silva
ProbNV: probabilistic verification of network control planes. 1-30 - Lukas Lazarek, Ben Greenman
How to evaluate blame for gradual types. 1-29 - Joshua Yanovski, Hoang-Hai Dang
GhostCell: separating permissions from data in Rust. 1-30 - Xuejing Huang
Distributing intersection and union types with splits and duality (functional pearl). 1-24 - David M. Kahn, Jan Hoffmann:
Automatic amortized resource analysis with the Quantum physicist's method. 1-29 - Martin Avanzini, Gilles Barthe
On continuation-passing transformations and expected cost analysis. 1-30 - Adam Chlipala
Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl). 1-28 - Mitchell Pickard, Graham Hutton
Calculating dependently-typed compilers (functional pearl). 1-27 - Farzin Houshmand, Mohsen Lesani, Keval Vora
Grafs: declarative graph analytics. 1-32 - Richard A. Eisenberg
An existential crisis resolved: type inference for first-class existential types. 1-29 - Zesen Qian, G. A. Kavvos
Client-server sessions in linear logic. 1-31 - Yasunari Watanabe, Kiran Gopinathan, George Pîrlea
Certifying the synthesis of heap-manipulating programs. 1-29 - John M. Li
Deriving efficient program transformations from rewrite rules. 1-29 - Yao Li
Reasoning about the garden of forking paths. 1-28
Volume 5, Number OOPSLA, October 2021
- Jialu Zhang, Ruzica Piskac
Static detection of silent misconfigurations with deep interaction analysis. 1-30 - Zhe Zhou
Data-driven abductive inference of library specifications. 1-29 - Aviral Goel
What we eval in the shadows: a large-scale study of eval in R programs. 1-23 - Kevin De Porre
ECROs: building global scale systems from sequential code. 1-30 - Son Tuan Vu, Albert Cohen
Reconciling optimization with secure compilation. 1-30 - Rawn Henry, Olivia Hsu
Compilation of sparse array programming models. 1-29 - Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, Yannis Smaragdakis:
Making pointer analysis more precise by unleashing the power of selective context sensitivity. 1-27 - Angelica Aparecida Moreira
VESPA: static profiling for binary optimization. 1-28 - Milod Kazerounian, Jeffrey S. Foster, Bonan Min:
SimTyper: sound type inference for Ruby using type equality prediction. 1-27 - Kasra Ferdowsifard
LooPy: interactive program synthesis with control structures. 1-29 - Malte Viering, Raymond Hu
A multiparty session typing discipline for fault-tolerant event-driven distributed programming. 1-30 - Wolf Honoré
Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. 1-31 - Georgios Karachalias, Filip Koprivec
Efficient compilation of algebraic effect handlers. 1-28 - Haoran Xu, Fredrik Kjolstad
Copy-and-patch compilation: a fast compilation algorithm for high-level languages and bytecode. 1-30 - Nader Al Awar, Kush Jain, Christopher J. Rossbach
Programming and execution models for parallel bounded exhaustive testing. 1-28 - Ziqiao Zhou, Michael K. Reiter:
Interpretable noninterference measurement and its application to processor designs. 1-30 - Yuyan Bao
Reachability types: tracking aliasing and separation in higher-order functional programs. 1-32 - Chandrakana Nandi, Max Willsey
Rewrite rule inference using equality saturation. 1-28 - Artem Pelenitsyn
Type stability in Julia: avoiding performance pathologies in JIT compilation. 1-26 - Kia Rahmani, Mohammad Raza, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna
Multi-modal program inference: a marriage of pre-trained language models and component-based synthesis. 1-29 - Ting Su
Fully automated functional fuzzing of Android apps for detecting non-crashing logic bugs. 1-31 - Pengbo Yan
SecRSL: security separation logic for C11 release-acquire concurrency. 1-26 - Jiwon Park, Dominik Winterer
Generative type-aware mutation for testing SMT solvers. 1-19 - Fabian Wolff, Aurel Bílý
Modular specification and verification of closures in Rust. 1-29 - Angello Astorga
Synthesizing contracts correct modulo a test generator. 1-27 - Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Mitropoulos, Dimitris Mitropoulos, Diomidis Spinellis
Well-typed programs can go wrong: a study of typing-related bugs in JVM compilers. 1-30 - Tyler Sorensen
Specifying and testing GPU workgroup progress models. 1-30 - Ori Roth
Study of the subtyping machine of nominal subtyping with variance. 1-27 - Xiaodong Jia
A derivative-based parser generator for visibly Pushdown grammars. 1-24 - Satyajit Gokhale, Alexi Turcotte, Frank Tip:
Automatic migration from synchronous to asynchronous JavaScript APIs. 1-27 - Mohamad Barbar, Yulei Sui
Compacting points-to sets through object clustering. 1-27 - Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, Christopher S. Meiklejohn:
Durable functions: semantics for stateful serverless. 1-27 - Gust Verbruggen
Semantic programming by example with pre-trained models. 1-25 - Guoqiang Zhang, Yuanchao Xu
UDF to SQL translation through compositional lazy inductive synthesis. 1-26 - Karl Cronburg
Permchecker: a toolchain for debugging memory managers with typestate. 1-28 - Christian Bräm, Marco Eilers
Rich specifications for Ethereum smart contract verification. 1-30 - Ori Lahav
Making weak memory models fair. 1-27 - Dan Iorga
The semantics of shared memory in Intel CPU/FPGA systems. 1-28 - Xipeng Shen
Coarsening optimization for differentiable programming. 1-27 - Xiang Gao, Arjun Radhakrishna
APIfix: output-oriented program synthesis for combating breaking changes in libraries. 1-27 - Fabian Muehlboeck
Transitioning from structural to nominal code with efficient gradual typing. 1-29 - Ruyi Ji, Jingtao Xia, Yingfei Xiong, Zhenjiang Hu:
Generalizable synthesis through unification. 1-28 - Sándor Bartha
One down, 699 to go: or, synthesising compositional desugarings. 1-29 - Truc Lam Bui, Krishnendu Chatterjee
The reads-from equivalence for the TSO and PSO memory models. 1-30 - Alexandru Dura
JavaDL: automatically incrementalizing Java bug pattern detection. 1-31 - Justin Lubin
How statically-typed functional programmers write code. 1-30 - Florian Lanzinger
Scalability and precision by combining expressive type systems and deductive verification. 1-29 - Peisen Yao
Program analysis via efficient symbolic abstraction. 1-32 - Didier Ishimwe
Dynaplex: analyzing program complexity using dynamically inferred recurrence relations. 1-23 - Zoe Paraskevopoulou, Anvay Grover:
Compiling with continuations, correctly. 1-29 - Aviral Goel
Promises are made to be broken: migrating R to strict semantics. 1-20 - Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, Jonathan Ragan-Kelley:
Efficient automatic scheduling of imaging and vision pipelines for the GPU. 1-28 - Rohan Bavishi, Caroline Lemieux, Koushik Sen, Ion Stoica:
Gauss: program synthesis by reasoning over graphs. 1-29 - Nouraldin Jaber, Christopher Wagner, Swen Jacobs
QuickSilver: modeling and parameterized verification for distributed agreement-based systems. 1-31 - Robert Brotzman, Danfeng Zhang
SpecSafe: detecting cache side channels in a speculative world. 1-28 - Weili Fu, Fabian Krause
Label dependent lambda calculus and gradual typing. 1-29 - Michael D. Brown
Not so fast: understanding and mitigating negative impacts of compiler optimizations on code reuse gadget sets. 1-30 - Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, Tobias Grosser
FPL: fast Presburger arithmetic through transprecision. 1-26 - Mehmet Emre
Translating C to safer Rust. 1-29 - Magnus Madsen, Jaco van de Pol:
Relational nullable types with Boolean unification. 1-28 - Guy L. Steele Jr.
LXM: better splittable pseudorandom number generators (and almost as fast). 1-31 - Natalie Popescu, Ziyang Xu
Safer at any speed: automatic context-aware safety enhancement for Rust. 1-23 - Nisarg Patel, Siddharth Krishna, Dennis E. Shasha, Thomas Wies:
Verifying concurrent multicopy search structures. 1-32 - Yann Herklotz
Formal verification of high-level synthesis. 1-30 - Masaomi Yamaguchi
Synbit: synthesizing bidirectional programs using unidirectional sketches. 1-31 - Eric Atkinson
Statically bounded-memory delayed sampling for probabilistic streams. 1-28 - Luna Phipps-Costin, Carolyn Jane Anderson
Solver-based gradual type migration. 1-27 - Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos
Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts. 1-30 - Paul He
A type system for extracting functional specifications from memory-safe imperative programs. 1-29 - Stefan Malewski
Gradually structured data. 1-29 - Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, Akash Lal:
MonkeyDB: effectively testing correctness under weak isolation levels. 1-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-02-13 00:55 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: