


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 David Margalit

, Ori Lahav
:
Verifying observational robustness against a c11-style memory model. 1-33 - Frantisek Farka

, Aleksandar Nanevski
, Anindya Banerjee
, Germán Andrés Delbianco
, Ignacio Fábregas
:
On algebraic abstractions for concurrent separation logics. 1-32 - Aïna Linn Georges

, Armaël Guéneau, Thomas Van Strydonck, Amin Timany
, Alix Trieu
, Sander Huyghebaert
, Dominique Devriese
, Lars Birkedal
:
Efficient and provable local capability revocation using uninitialized capabilities. 1-30 - Koen Jacobs

, Amin Timany
, Dominique Devriese
:
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

, Amr Sabry
:
A computational interpretation of compact closed categories: reversible programming with negative and fractional types. 1-29 - Simon Oddershede Gregersen

, Johan Bay, Amin Timany
, Lars Birkedal
:
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

, Evan Cavallo
, Anders Mörtberg, Max Zeuner
:
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

, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Learning the boundary of inductive invariants. 1-30 - Silvia Ghilezan

, Jovanka Pantovic
, Ivan Prokic
, Alceste Scalas
, Nobuko Yoshida
:
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

, Sam Westrick
, Umut A. Acar:
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

, Eric Mark Martin, Dominique Devriese
:
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

, Chandrakana Nandi, Yisu Remy Wang
, Oliver Flatt, Zachary Tatlock
, Pavel Panchekha:
egg: Fast and extensible equality saturation. 1-29 - Danel Ahman

, Matija Pretnar
:
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

, Marco Gaboardi
, Deepak Garg
, Jan Hoffmann:
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

, Mridul Aanjaneya
, John L. Gustafson, Santosh Nagarakatte
:
An approach to generate correctly rounded math libraries for new floating point variants. 1-30 - Jinwoo Kim

, Qinheping Hu, Loris D'Antoni, Thomas W. Reps:
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

, Claudia Faggian, Simona Ronchi Della Rocca:
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

, Ethan Cecchetti
:
Giving semantics to program-counter labels via secure effects. 1-29 - Umang Mathur

, Andreas Pavlogiannis
, Mahesh Viswanathan:
Optimal prediction of synchronization-preserving races. 1-29 - Kesha Hietala

, Robert Rand
, Shih-Han Hung
, Xiaodi Wu, Michael Hicks
:
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

, Benjamin Lucien Kaminski
, Joost-Pieter Katoen
, Christoph Matheja
:
Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. 1-30 - Nathanaël Courant

, Xavier Leroy
:
Verified code generation for the polyhedral model. 1-24 - Ryan Doenges

, Mina Tahmasbi Arashloo, Santiago Bautista
, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin
, Amanda Xu, Nate Foster:
Petr4: formal foundations for p4 data planes. 1-32 - Léon Gondelman, Simon Oddershede Gregersen

, Abel Nieto
, Amin Timany
, Lars Birkedal
:
Distributed causal memory: modular specification and verification in higher-order distributed separation logic. 1-29 - Michalis Kokologiannakis

, Ilya Kaysin
, Azalea Raad, Viktor Vafeiadis
:
PerSeVerE: persistency semantics for verification under ext4. 1-29 - Pascal Baumann

, Rupak Majumdar
, Ramanathan S. Thinniyam
, Georg Zetzsche
:
Context-bounded verification of liveness properties for multithreaded shared-memory programs. 1-31 - Alban Reynaud, Gabriel Scherer

, Jeremy Yallop:
A practical mode system for recursive definitions. 1-29 - Aurèle Barrière

, Sandrine Blazy
, Olivier Flückiger
, David Pichardie, Jan Vitek:
Formally verified speculation and deoptimization in a JIT compiler. 1-26 - Artem Khyzha, Ori Lahav

:
Taming x86-TSO persistency. 1-29 - Shaull Almagor

, Toghrul Karimov
, Edon Kelmendi, Joël Ouaknine, James Worrell:
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

, Deian Stefan:
Automatically eliminating speculative leaks from cryptographic code with blade. 1-30 - Pritam Choudhury, Harley Eades III, Richard A. Eisenberg

, Stephanie Weirich:
A graded dependent type system with a usage-aware semantics. 1-32 - Beniamino Accattoli, Ugo Dal Lago

, Gabriele Vanoni
:
The (In)Efficiency of interaction. 1-33 - Alejandro Aguirre

, Gilles Barthe, Justin Hsu
, Benjamin Lucien Kaminski
, Joost-Pieter Katoen
, Christoph Matheja
:
A pre-expectation calculus for probabilistic sensitivity. 1-28 - Cameron Moy

, Phuc C. Nguyen, Sam Tobin-Hochstadt
, David Van Horn
:
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

, Steven J. Ramsay
:
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

, Fosco Loregiàn
, Chad Nester, Pawel Sobocinski:
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
, Thomas W. Reps:
On the complexity of bidirected interleaved Dyck-reachability. 1-28 - Jesper Cockx, Nicolas Tabareau

, Théo Winterhalter
:
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

, Nicolas Wu
:
Algebras for weighted search. 1-30 - Zhixuan Yang

, Nicolas Wu
:
Reasoning about effect interaction by fusion. 1-29 - Zoe Paraskevopoulou, John M. Li, Andrew W. Appel

:
Compositional optimizations for CertiCoq. 1-30 - Nikita Zyuzin

, Aleksandar Nanevski
:
Contextual modal types for algebraic effects and handlers. 1-29 - Alejandro Aguirre

, Gilles Barthe
, Marco Gaboardi
, Deepak Garg
, Shin-ya Katsumata
, Tetsuya Sato
:
Higher-order probabilistic adversarial computations: categorical semantics and program logics. 1-30 - Kimball Germane

, Jay McCarthy:
Newly-single and loving it: improving higher-order must-alias analysis with heap fragments. 1-28 - Chaitanya Koparkar, Mike Rainey, Michael Vollmer, Milind Kulkarni

, Ryan R. Newton:
Efficient tree-traversals: reconciling parallelism and dense data representations. 1-29 - Glen Mével

, Jacques-Henri Jourdan
:
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

, Tahina Ramananandro
:
Steel: proof-oriented programming in a dependently typed concurrent separation logic. 1-30 - Sandro Stucki

, Paolo G. Giarrusso
:
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

, Thomas Dinsdale-Young, Armaël Guéneau
, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos:
Theorems for free from separation logic specifications. 1-29 - Yannick Zakowski

, Calvin Beck
, Irene Yoon
, Ilia Zaichuk
, Vadim Zaliva
, Steve Zdancewic
:
Modular, compositional, and executable formal semantics for LLVM IR. 1-30 - Denis Merigoux

, Nicolas Chataing, Jonathan Protzenko:
Catala: a programming language for the law. 1-29 - Nicolas Krauter

, Patrick Raaf
, Peter Braam, Reza Salkhordeh
, Sebastian Erdweg
, André Brinkmann:
Persistent software transactional memory in Haskell. 1-29 - Taro Sekiyama

, Takeshi Tsukada
:
CPS transformation with affine types for call-by-value implicit polymorphism. 1-30 - Nick Giannarakis, Alexandra Silva

, David Walker
:
ProbNV: probabilistic verification of network control planes. 1-30 - Lukas Lazarek

, Ben Greenman
, Matthias Felleisen, Christos Dimoulas
:
How to evaluate blame for gradual types. 1-29 - Joshua Yanovski, Hoang-Hai Dang

, Ralf Jung
, Derek Dreyer:
GhostCell: separating permissions from data in Rust. 1-30 - Xuejing Huang

, Bruno C. d. S. Oliveira:
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

, Ugo Dal Lago
:
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

, Guillaume Duboc, Stephanie Weirich
, Daniel Lee:
An existential crisis resolved: type inference for first-class existential types. 1-29 - Zesen Qian, G. A. Kavvos

, Lars Birkedal
:
Client-server sessions in linear logic. 1-31 - Yasunari Watanabe, Kiran Gopinathan, George Pîrlea

, Nadia Polikarpova
, Ilya Sergey
:
Certifying the synthesis of heap-manipulating programs. 1-29 - John M. Li

, Andrew W. Appel
:
Deriving efficient program transformations from rewrite rules. 1-29 - Yao Li

, Li-yao Xia
, Stephanie Weirich
:
Reasoning about the garden of forking paths. 1-28
Volume 5, Number OOPSLA, October 2021
- Jialu Zhang, Ruzica Piskac

, Ennan Zhai, Tianyin Xu
:
Static detection of silent misconfigurations with deep interaction analysis. 1-30 - Zhe Zhou

, Robert Dickerson
, Benjamin Delaware, Suresh Jagannathan:
Data-driven abductive inference of library specifications. 1-29 - Aviral Goel

, Pierre Donat-Bouillud
, Filip Krikava, Christoph M. Kirsch, Jan Vitek:
What we eval in the shadows: a large-scale study of eval in R programs. 1-23 - Kevin De Porre

, Carla Ferreira
, Nuno M. Preguiça
, Elisa Gonzalez Boix
:
ECROs: building global scale systems from sequential code. 1-30 - Son Tuan Vu, Albert Cohen

, Arnaud de Grandmaison, Christophe Guillon, Karine Heydemann:
Reconciling optimization with secure compilation. 1-30 - Rawn Henry, Olivia Hsu

, Rohan Yadav
, Stephen Chou, Kunle Olukotun
, Saman P. Amarasinghe, Fredrik Kjolstad
:
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

, Guilherme Ottoni, Fernando Magno Quintão Pereira
:
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

, Shraddha Barke
, Hila Peleg
, Sorin Lerner
, Nadia Polikarpova
:
LooPy: interactive program synthesis with control structures. 1-29 - Malte Viering, Raymond Hu

, Patrick Eugster
, Lukasz Ziarek:
A multiparty session typing discipline for fault-tolerant event-driven distributed programming. 1-30 - Wolf Honoré

, Jieung Kim
, Ji-Yong Shin
, Zhong Shao
:
Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. 1-31 - Georgios Karachalias, Filip Koprivec

, Matija Pretnar
, Tom Schrijvers
:
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

, Milos Gligoric:
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

, Guannan Wei
, Oliver Bracevac
, Yuxuan Jiang
, Qiyang He, Tiark Rompf:
Reachability types: tracking aliasing and separation in higher-order functional programs. 1-32 - Chandrakana Nandi, Max Willsey

, Amy Zhu, Yisu Remy Wang
, Brett Saiki
, Adam Anderson, Adriana Schulz
, Dan Grossman, Zachary Tatlock
:
Rewrite rule inference using equality saturation. 1-28 - Artem Pelenitsyn

, Julia Belyakova
, Benjamin Chung
, Ross Tate
, Jan Vitek
:
Type stability in Julia: avoiding performance pathologies in JIT compilation. 1-26 - Kia Rahmani, Mohammad Raza, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna

, Gustavo Soares, Ashish Tiwari:
Multi-modal program inference: a marriage of pre-trained language models and component-based synthesis. 1-29 - Ting Su

, Yichen Yan, Jue Wang
, Jingling Sun
, Yiheng Xiong, Geguang Pu, Ke Wang, Zhendong Su:
Fully automated functional fuzzing of Android apps for detecting non-crashing logic bugs. 1-31 - Pengbo Yan

, Toby Murray
:
SecRSL: security separation logic for C11 release-acquire concurrency. 1-26 - Jiwon Park, Dominik Winterer

, Chengyu Zhang
, Zhendong Su:
Generative type-aware mutation for testing SMT solvers. 1-19 - Fabian Wolff, Aurel Bílý

, Christoph Matheja
, Peter Müller
, Alexander J. Summers
:
Modular specification and verification of closures in Rust. 1-29 - Angello Astorga

, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan
, Tao Xie
:
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

, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson
, Margaret Martonosi, Alastair F. Donaldson
:
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

, Ashish Kumar
, Gang Tan
:
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

, Vu Le, Sumit Gulwani:
Semantic programming by example with pre-trained models. 1-25 - Guoqiang Zhang, Yuanchao Xu

, Xipeng Shen
, Isil Dillig:
UDF to SQL translation through compositional lazy inductive synthesis. 1-26 - Karl Cronburg

, Samuel Z. Guyer:
Permchecker: a toolchain for debugging memory managers with typestate. 1-28 - Christian Bräm, Marco Eilers

, Peter Müller
, Robin Sierra, Alexander J. Summers
:
Rich specifications for Ethereum smart contract verification. 1-30 - Ori Lahav

, Egor Namakonov
, Jonas Oberhauser, Anton Podkopaev
, Viktor Vafeiadis
:
Making weak memory models fair. 1-27 - Dan Iorga

, Alastair F. Donaldson
, Tyler Sorensen
, John Wickerson
:
The semantics of shared memory in Intel CPU/FPGA systems. 1-28 - Xipeng Shen

, Guoqiang Zhang, Irene Dea, Samantha Andow, Emilio Arroyo-Fang, Neal Gafter, Johann George, Melissa Grueter, Erik Meijer, Olin Grigsby Shivers, Steffi Stumpos, Alanna Tempest, Christy Warden, Shannon Yang:
Coarsening optimization for differentiable programming. 1-27 - Xiang Gao

, Arjun Radhakrishna
, Gustavo Soares, Ridwan Shariffdeen
, Sumit Gulwani, Abhik Roychoudhury
:
APIfix: output-oriented program synthesis for combating breaking changes in libraries. 1-27 - Fabian Muehlboeck

, Ross Tate
:
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

, James Cheney
, Vaishak Belle
:
One down, 699 to go: or, synthesising compositional desugarings. 1-29 - Truc Lam Bui, Krishnendu Chatterjee

, Tushar Gautam, Andreas Pavlogiannis
, Viktor Toman
:
The reads-from equivalence for the TSO and PSO memory models. 1-30 - Alexandru Dura

, Christoph Reichenbach
, Emma Söderberg
:
JavaDL: automatically incrementalizing Java bug pattern detection. 1-31 - Justin Lubin

, Sarah E. Chasins
:
How statically-typed functional programmers write code. 1-30 - Florian Lanzinger

, Alexander Weigl
, Mattias Ulbrich
, Werner Dietl
:
Scalability and precision by combining expressive type systems and deductive verification. 1-29 - Peisen Yao

, Qingkai Shi
, Heqing Huang, Charles Zhang:
Program analysis via efficient symbolic abstraction. 1-32 - Didier Ishimwe

, KimHao Nguyen
, ThanhVu Nguyen
:
Dynaplex: analyzing program complexity using dynamically inferred recurrence relations. 1-23 - Zoe Paraskevopoulou, Anvay Grover

:
Compiling with continuations, correctly. 1-29 - Aviral Goel

, Jan Jecmen, Sebastián Krynski, Olivier Flückiger
, Jan Vitek
:
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

, Milind Kulkarni
, Roopsha Samanta:
QuickSilver: modeling and parameterized verification for distributed agreement-based systems. 1-31 - Robert Brotzman, Danfeng Zhang

, Mahmut Taylan Kandemir, Gang Tan
:
SpecSafe: detecting cache side channels in a speculative world. 1-28 - Weili Fu, Fabian Krause

, Peter Thiemann
:
Label dependent lambda calculus and gradual typing. 1-29 - Michael D. Brown

, Matthew Pruett, Robert Bigelow, Girish Mururu, Santosh Pande
:
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

, Ryan Schroeder
, Kyle Dewey
, Ben Hardekopf
:
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.

, Sebastiano Vigna
:
LXM: better splittable pseudorandom number generators (and almost as fast). 1-31 - Natalie Popescu

, Ziyang Xu
, Sotiris Apostolakis, David I. August, Amit Levy
:
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

, James D. Pollard
, Nadesh Ramanathan
, John Wickerson
:
Formal verification of high-level synthesis. 1-30 - Masaomi Yamaguchi

, Kazutaka Matsuda
, Cristina David
, Meng Wang
:
Synbit: synthesizing bidirectional programs using unidirectional sketches. 1-31 - Eric Atkinson

, Guillaume Baudart, Louis Mandel, Charles Yuan
, Michael Carbin
:
Statically bounded-memory delayed sampling for probabilistic streams. 1-28 - Luna Phipps-Costin, Carolyn Jane Anderson

, Michael Greenberg
, Arjun Guha
:
Solver-based gradual type migration. 1-27 - Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos

, Konstantinos Triantafyllou, Ilias Tsatiris
:
Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts. 1-30 - Paul He

, Eddy Westbrook, Brent Carmer, Chris Phifer
, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic
:
A type system for extracting functional specifications from memory-safe imperative programs. 1-29 - Stefan Malewski

, Michael Greenberg
, Éric Tanter:
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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














