Last update:
Sat Jul 1 10:28:58 MDT 2023
Philip Wadler Editorial message . . . . . . . . . . . 1:1--1:??
Vincent St-Amour and
Daniel Feltey and
Spencer P. Florence and
Shu-Hung You and
Robert Bruce Findler \bionameHerbarium Racketensis: a stroll
through the woods (functional pearl) . . 1:1--1:??
Ivan Perez and
Henrik Nilsson Testing and debugging functional
reactive programming . . . . . . . . . . 2:1--2:??
Joachim Breitner and
Chris Smith Lock-step simulation is child's play
(experience report) . . . . . . . . . . 3:1--3:??
Benjamin Canou and
Roberto Di Cosmo and
Grégoire Henry Scaling up functional programming
education: under the hood of the OCaml
MOOC . . . . . . . . . . . . . . . . . . 4:1--4:??
Michael Spivey Faster coroutine pipelines . . . . . . . 5:1--5:??
Jean-Philippe Bernardy A pretty but not greedy printer
(functional pearl) . . . . . . . . . . . 6:1--6:??
Conal Elliott Generic functional parallel algorithms:
scan and FFT . . . . . . . . . . . . . . 7:1--7:??
William E. Byrd and
Michael Ballantyne and
Gregory Rosenblatt and
Matthew Might A unified approach to solving seven
programming problems (functional pearl) 8:1--8:??
Joshua S. Auerbach and
Martin Hirzel and
Louis Mandel and
Avraham Shinnar and
Jérôme Siméon Prototyping a query compiler using Coq
(experience report) . . . . . . . . . . 9:1--9:??
Daniel Winograd-Cort and
Andreas Haeberlen and
Aaron Roth and
Benjamin C. Pierce A framework for adaptive differential
privacy . . . . . . . . . . . . . . . . 10:1--10:??
Praveen Narayanan and
Chung-chieh Shan Symbolic conditioning of arrays in
probabilistic programs . . . . . . . . . 11:1--11:??
David Darais and
Nicholas Labich and
Phúc C. Nguyen and
David Van Horn Abstracting definitional interpreters
(functional pearl) . . . . . . . . . . . 12:1--12:??
Yannick Forster and
Ohad Kammar and
Sam Lindley and
Matija Pretnar On the expressive power of user-defined
effects: effect handlers, monadic
reflection, delimited control . . . . . 13:1--13:??
Wilmer Ricciotti and
Jan Stolarek and
Roly Perera and
James Cheney Imperative functional programs that
explain their work . . . . . . . . . . . 14:1--14:??
Jan Midtgaard and
Mathias Nygaard Justesen and
Patrick Kasting and
Flemming Nielson and
Hanne Riis Nielson Effect-driven QuickChecking of compilers 15:1--15:??
Juan Pedro Bolívar Puente Persistence for the masses: RRB-vectors
in a systems language . . . . . . . . . 16:1--16:??
Jonathan Protzenko and
Jean-Karim Zinzindohoué and
Aseem Rastogi and
Tahina Ramananandro and
Peng Wang and
Santiago Zanella-Béguelin and
Antoine Delignat-Lavaud and
Catalin Hritcu and
Karthikeyan Bhargavan and
Cédric Fournet and
Nikhil Swamy Verified low-level programming embedded
in F* . . . . . . . . . . . . . . . . . 17:1--17:??
Scott Owens and
Michael Norrish and
Ramana Kumar and
Magnus O. Myreen and
Yong Kiam Tan Verifying efficient function calls in
CakeML . . . . . . . . . . . . . . . . . 18:1--18:??
Geoffrey Mainland Better living through operational
semantics: an optimizing compiler for
radio protocols . . . . . . . . . . . . 19:1--19:??
Thibaut Balabonski and
Pablo Barenbaum and
Eduardo Bonelli and
Delia Kesner Foundations of strong call by need . . . 20:1--20:??
Alejandro Aguirre and
Gilles Barthe and
Marco Gaboardi and
Deepak Garg and
Pierre-Yves Strub A relational logic for higher-order
programs . . . . . . . . . . . . . . . . 21:1--21:??
Makoto Hamana How to prove your calculus is decidable:
practical applications of second-order
algebraic theories and computation . . . 22:1--22:??
Milo Davis and
William Meehan and
Olin Shivers No-brainer CPS conversion (functional
pearl) . . . . . . . . . . . . . . . . . 23:1--23:??
Joonwon Choi and
Muralidaran Vijayaraghavan and
Benjamin Sherman and
Adam Chlipala and
Arvind Kami: a platform for high-level
parametric hardware specification and
its modular verification . . . . . . . . 24:1--24:??
Konstantin Weitz and
Steven Lyubomirsky and
Stefan Heule and
Emina Torlak and
Michael D. Ernst and
Zachary Tatlock SpaceSearch: a library for building and
verifying solver-aided tools . . . . . . 25:1--25:??
Benjamin Cosman and
Ranjit Jhala Local refinement typing . . . . . . . . 26:1--26:??
Conal Elliott Compiling to categories . . . . . . . . 27:1--27:??
François Pottier Visitors unchained . . . . . . . . . . . 28:1--28:??
Jeremy Yallop Staged generic programming . . . . . . . 29:1--29:??
Leif Andersen and
Stephen Chang and
Matthias Felleisen Super 8 languages for making movies
(functional pearl) . . . . . . . . . . . 30:1--30:??
Stephanie Weirich and
Antoine Voizard and
Pedro Henrique Azevedo de Amorim and
Richard A. Eisenberg A specification for dependent types in
Haskell . . . . . . . . . . . . . . . . 31:1--31:??
Andreas Nuyts and
Andrea Vezzosi and
Dominique Devriese Parametric quantifiers for dependent
type theory . . . . . . . . . . . . . . 32:1--32:??
Andreas Abel and
Andrea Vezzosi and
Theo Winterhalter Normalization by evaluation for sized
dependent types . . . . . . . . . . . . 33:1--33:??
Gabriel Ebner and
Sebastian Ullrich and
Jared Roesch and
Jeremy Avigad and
Leonardo de Moura A metaprogramming framework for formal
verification . . . . . . . . . . . . . . 34:1--34:??
Hernán Melgratti and
Luca Padovani Chaperone contracts for higher-order
sessions . . . . . . . . . . . . . . . . 35:1--35:??
Lucas Waye and
Stephen Chong and
Christos Dimoulas Whip: higher-order contracts for modern
services . . . . . . . . . . . . . . . . 36:1--36:??
Stephanie Balzer and
Frank Pfenning Manifest sharing with session types . . 37:1--37:??
Atsushi Igarashi and
Peter Thiemann and
Vasco T. Vasconcelos and
Philip Wadler Gradual session types . . . . . . . . . 38:1--38:??
Amal Ahmed and
Dustin Jamner and
Jeremy G. Siek and
Philip Wadler Theorems for free for free:
parametricity, with and without types 39:1--39:??
Yuu Igarashi and
Taro Sekiyama and
Atsushi Igarashi On polymorphic gradual typing . . . . . 40:1--40:??
Giuseppe Castagna and
Victor Lanvin Gradual typing with union and
intersection types . . . . . . . . . . . 41:1--41:??
J. Garrett Morris and
Richard A. Eisenberg Constrained type families . . . . . . . 42:1--42:??
Martin Avanzini and
Ugo Dal Lago Automating sized-type inference for
complexity analysis . . . . . . . . . . 43:1--43:??
Justin Pombrio and
Shriram Krishnamurthi and
Mitchell Wand Inferring scope through syntactic sugar 44:1--44:??
Izzat El Hajj and
Thomas B. Jablin and
Dejan Milojicic and
Wen-mei Hwu SAVI objects: sharing and virtuality
incorporated . . . . . . . . . . . . . . 45:1--45:??
Marianna Rapoport and
Ifaz Kabir and
Paul He and
Ondrej Lhoták A simple soundness proof for dependent
object types . . . . . . . . . . . . . . 46:1--46:??
Yanpeng Yang and
Bruno C. d. S. Oliveira Unifying typing and subtyping . . . . . 47:1--47:??
Avik Chaudhuri and
Panagiotis Vekris and
Sam Goldman and
Marshall Roch and
Gabriel Levi Fast and precise type checking for
JavaScript . . . . . . . . . . . . . . . 48:1--48:??
Lun Liu and
Todd Millstein and
Madanlal Musuvathi A volatile-by-default JVM for server
applications . . . . . . . . . . . . . . 49:1--49:??
Gabriel Poesia and
Breno Guimarães and
Fabrício Ferracioli and
Fernando Magno Quintão Pereira Static placement of computation on
heterogeneous devices . . . . . . . . . 50:1--50:??
Sarah Chasins and
Rastislav Bodik Skip blocks: reusing execution history
to accelerate web scripts . . . . . . . 51:1--51:??
Edd Barrett and
Carl Friedrich Bolz-Tereick and
Rebecca Killick and
Sarah Mount and
Laurence Tratt Virtual machine warmup blows hot and
cold . . . . . . . . . . . . . . . . . . 52:1--52:??
Tomoharu Ugawa and
Tatsuya Abe and
Toshiyuki Maeda Model checking copy phases of concurrent
copying garbage collection with various
memory models . . . . . . . . . . . . . 53:1--53:??
Spenser Bauman and
Carl Friedrich Bolz-Tereick and
Jeremy Siek and
Sam Tobin-Hochstadt Sound gradual typing: only mostly dead 54:1--54:??
Gregor Richards and
Ellen Arteca and
Alexi Turcotte The VM already knew that: leveraging
compile-time knowledge to optimize
gradual typing . . . . . . . . . . . . . 55:1--55:??
Fabian Muehlboeck and
Ross Tate Sound gradual typing is nominally alive
and well . . . . . . . . . . . . . . . . 56:1--56:??
Xin Zhang and
Radu Grigore and
Xujie Si and
Mayur Naik Effective interactive resolution of
static analysis alarms . . . . . . . . . 57:1--57:??
Binhang Yuan and
Vijayaraghavan Murali and
Christopher Jermaine Abridging source code . . . . . . . . . 58:1--58:??
Guilherme Cavalcanti and
Paulo Borba and
Paola Accioly Evaluating and improving semistructured
merge . . . . . . . . . . . . . . . . . 59:1--59:??
Eric L. Seidel and
Huma Sibghat and
Kamalika Chaudhuri and
Westley Weimer and
Ranjit Jhala Learning to blame: localizing novice
type errors with data-driven diagnosis 60:1--60:??
Venkatesh Srinivasan and
Ara Vartanian and
Thomas Reps Model-assisted machine-code synthesis 61:1--61:??
Xinyu Wang and
Isil Dillig and
Rishabh Singh Synthesis of data completion scripts
using finite tree automata . . . . . . . 62:1--62:??
Navid Yaghmazadeh and
Yuepeng Wang and
Isil Dillig and
Thomas Dillig SQLizer: query synthesis from natural
language . . . . . . . . . . . . . . . . 63:1--63:??
Mark Santolucito and
Ennan Zhai and
Rahul Dhodapkar and
Aaron Shim and
Ruzica Piskac Synthesizing configuration file
specifications with association rule
learning . . . . . . . . . . . . . . . . 64:1--64:??
Xiaokang Qiu and
Armando Solar-Lezama Natural synthesis of provably-correct
data-structure manipulations . . . . . . 65:1--65:??
Christoffer Quist Adamsen and
Anders Mòller and
Frank Tip Practical initialization race detection
for JavaScript web applications . . . . 66:1--66:??
Nachshon Cohen and
Michal Friedman and
James R. Larus Efficient logging in non-volatile memory
by exploiting coherency protocols . . . 67:1--67:??
Neville Grech and
George Fourtounis and
Adrian Francalanza and
Yannis Smaragdakis Heaps don't lie: countering unsoundness
with heap snapshots . . . . . . . . . . 68:1--68:??
Benjamin P. Wood and
Man Cao and
Michael D. Bond and
Dan Grossman Instrumentation bias for dynamic data
race detection . . . . . . . . . . . . . 69:1--69:??
Yizhou Zhang and
Andrew C. Myers Familia: unifying interfaces, type
classes, and family polymorphism . . . . 70:1--70:??
Adrian Sampson and
Kathryn S. McKinley and
Todd Mytkowicz Static stages for heterogeneous
programming . . . . . . . . . . . . . . 71:1--71:??
Sylvan Clebsch and
Juliana Franco and
Sophia Drossopoulou and
Albert Mingkun Yang and
Tobias Wrigstad and
Jan Vitek Orca: GC and type system co-design for
actor languages . . . . . . . . . . . . 72:1--72:??
Ryan G. Scott and
Omar S. Navarro Leija and
Joseph Devietti and
Ryan R. Newton Monadic composition for deterministic,
parallel batch processing . . . . . . . 73:1--73:??
Yufei Ding and
Xipeng Shen GLORE: generalized loop redundancy
elimination upon LER-notation . . . . . 74:1--74:??
Dominic Orchard and
Mistral Contrastin and
Matthew Danish and
Andrew Rice Verifying spatial properties of array
computations . . . . . . . . . . . . . . 75:1--75:??
Laith Sakka and
Kirshanthan Sundararajah and
Milind Kulkarni TreeFuser: a framework for analyzing and
fusing general recursive tree traversals 76:1--76:??
Fredrik Kjolstad and
Shoaib Kamil and
Stephen Chou and
David Lugato and
Saman Amarasinghe The tensor algebra compiler . . . . . . 77:1--77:??
Manolis Papadakis and
Gilbert Louis Bernstein and
Rahul Sharma and
Alex Aiken and
Pat Hanrahan Seam: provably safe local edits on
graphs . . . . . . . . . . . . . . . . . 78:1--78:??
Peng Wang and
Di Wang and
Adam Chlipala TiML: a functional language for
practical complexity analysis with
invariants . . . . . . . . . . . . . . . 79:1--79:??
Aws Albarghouthi and
Loris D'Antoni and
Samuel Drews and
Aditya V. Nori FairSquare: probabilistic verification
of program fairness . . . . . . . . . . 80:1--80:??
Davide Ancona and
Francesco Dagnino and
Elena Zucca Reasoning on divergent computations with
coaxioms . . . . . . . . . . . . . . . . 81:1--81:??
Michael D. Adams and
Matthew Might Restricting grammars with tree automata 82:1--82:??
Samantha Syeda Khairunnesa and
Hoan Anh Nguyen and
Tien N. Nguyen and
Hridesh Rajan Exploiting implicit beliefs to resolve
sparse usage problem in usage-based
specification mining . . . . . . . . . . 83:1--83:??
Cristina V. Lopes and
Petr Maj and
Pedro Martins and
Vaibhav Saini and
Di Yang and
Jakub Zitny and
Hitesh Sajnani and
Jan Vitek Déj\`aVu: a map of code duplicates on
GitHub . . . . . . . . . . . . . . . . . 84:1--84:??
Davood Mazinanian and
Ameya Ketkar and
Nikolaos Tsantalis and
Danny Dig Understanding the use of lambda
expressions in Java . . . . . . . . . . 85:1--85:??
Magnus Madsen and
Ondrej Lhoták and
Frank Tip A model for reasoning about JavaScript
promises . . . . . . . . . . . . . . . . 86:1--86:??
William Mansky and
Andrew W. Appel and
Aleksey Nogin A verified messaging system . . . . . . 87:1--87:??
Alastair Reid Who guards the guards? Formal validation
of the ARM v8-m architecture
specification . . . . . . . . . . . . . 88:1--88:??
David Swasey and
Deepak Garg and
Derek Dreyer Robust and compositional verification of
object capability patterns . . . . . . . 89:1--89:??
Erik Krogh Kristensen and
Anders Mòller Type test scripts for TypeScript testing 90:1--90:??
Talia Ringer and
Dan Grossman and
Daniel Schwartz-Narbonne and
Serdar Tasiran A solver-aided language for test input
generation . . . . . . . . . . . . . . . 91:1--91:??
Xia Li and
Lingming Zhang Transforming programs and tests in
tandem for fault localization . . . . . 92:1--92:??
Alastair F. Donaldson and
Hugues Evrard and
Andrei Lascu and
Paul Thomson Automated testing of graphics shader
compilers . . . . . . . . . . . . . . . 93:1--93:??
Ahmet Celik and
Sreepathi Pai and
Sarfraz Khurshid and
Milos Gligoric Bounded exhaustive test-input generation
on GPUs . . . . . . . . . . . . . . . . 94:1--94:??
Matthew Parkinson and
Dimitrios Vytiniotis and
Kapil Vaswani and
Manuel Costa and
Pantazis Deligiannis and
Dylan McDermott and
Aaron Blankstein and
Jonathan Balkind Project snowflake: non-blocking safe
manual memory management in .NET . . . . 95:1--95:??
Kiwan Maeng and
Alexei Colin and
Brandon Lucia Alpaca: intermittent execution without
checkpoints . . . . . . . . . . . . . . 96:1--96:??
Ennan Zhai and
Ruzica Piskac and
Ronghui Gu and
Xun Lao and
Xi Wang An auditing language for preventing
correlated failures in the cloud . . . . 97:1--97:??
Ted Kaminski and
Lucas Kramer and
Travis Carlson and
Eric Van Wyk Reliable and automatic composition of
language extensions to C: the ableC
extensible language framework . . . . . 98:1--98:??
Johannes Späth and
Karim Ali and
Eric Bodden IDEal: efficient and precise alias-aware
dataflow analysis . . . . . . . . . . . 99:1--99:??
Sehun Jeong and
Minseok Jeon and
Sungdeok Cha and
Hakjoo Oh Data-driven context-sensitivity for
points-to analysis . . . . . . . . . . . 100:1--100:??
Kwonsoo Chae and
Hakjoo Oh and
Kihong Heo and
Hongseok Yang Automatically generating features for
learning program analysis heuristics for
C-like languages . . . . . . . . . . . . 101:1--101:??
Neville Grech and
Yannis Smaragdakis P/Taint: unified points-to and taint
analysis . . . . . . . . . . . . . . . . 102:1--102:??
Tiago Cogumbreiro and
Rishi Surendran and
Francisco Martins and
Vivek Sarkar and
Vasco T. Vasconcelos and
Max Grossman Deadlock avoidance in parallel programs
with futures: why parallel tasks should
not wait for strangers . . . . . . . . . 103:1--103:??
Andrew Rice and
Edward Aftandilian and
Ciera Jaspan and
Emily Johnston and
Michael Pradel and
Yulissa Arroyo-Paredes Detecting argument selection defects . . 104:1--104:??
Baijun Wu and
Sheng Chen How type errors were fixed and what
students did? . . . . . . . . . . . . . 105:1--105:??
Baijun Wu and
John Peter Campora III and
Sheng Chen Learning user friendly type-error
messages . . . . . . . . . . . . . . . . 106:1--106:??
Philip A. Bernstein and
Sebastian Burckhardt and
Sergey Bykov and
Natacha Crooks and
Jose M. Faleiro and
Gabriel Kliot and
Alok Kumbhare and
Muntasir Raihan Rahman and
Vivek Shah and
Adriana Szekeres and
Jorgen Thelin Geo-distribution of actor-based services 107:1--107:??
Oded Padon and
Giuliano Losa and
Mooly Sagiv and
Sharon Shoham Paxos made EPR: decidable reasoning
about distributed protocols . . . . . . 108:1--108:??
Victor B. F. Gomes and
Martin Kleppmann and
Dominic P. Mulligan and
Alastair R. Beresford Verifying strong eventual consistency in
distributed systems . . . . . . . . . . 109:1--109:??
Alexander Bakst and
Klaus v. Gleissenthall and
Rami Gökhan Kici and
Ranjit Jhala Verifying distributed programs via
canonical sequentialization . . . . . . 110:1--110:??
Anders Miltner and
Kathleen Fisher and
Benjamin C. Pierce and
David Walker and
Steve Zdancewic Synthesizing bijective lenses . . . . . 1:1--1:??
Jeevana Priya Inala and
Rishabh Singh WebRelate: integrating web data with
spreadsheets using examples . . . . . . 2:1--2:??
Taolue Chen and
Yan Chen and
Matthew Hague and
Anthony W. Lin and
Zhilin Wu What is decidable about string
constraints with the ReplaceAll function 3:1--3:??
Luká\vs Holk and
Petr Jank\ru and
Anthony W. Lin and
Philipp Rümmer and
Tomá\vs Vojnar String constraints with concatenation
and transducers solved efficiently . . . 4:1--4:??
Jean-Philippe Bernardy and
Mathieu Boespflug and
Ryan R. Newton and
Simon Peyton Jones and
Arnaud Spiwack Linear Haskell: practical linearity in a
higher-order polymorphic language . . . 5:1--5:??
Damiano Mazza and
Luc Pellissier and
Pierre Vial Polyadic approximations, fibrations and
intersection types . . . . . . . . . . . 6:1--6:??
Danel Ahman Handling fibred algebraic effects . . . 7:1--7:??
Dariusz Biernacki and
Maciej Piróg and
Piotr Polesiuk and
Filip Sieczkowski Handle with care: relational
interpretation of algebraic effects and
handlers . . . . . . . . . . . . . . . . 8:1--8:??
Quang-Trung Ta and
Ton Chanh Le and
Siau-Cheng Khoo and
Wei-Ngan Chin Automated lemma synthesis in
symbolic-heap separation logic . . . . . 9:1--9:??
Christof Löding and
P. Madhusudan and
Lucas Peña Foundations for natural proofs and
quantifier instantiation . . . . . . . . 10:1--10:??
Toby Cathcart Burn and
C.-H. Luke Ong and
Steven J. Ramsay Higher-order constrained Horn clauses
for verification . . . . . . . . . . . . 11:1--11:??
Hiroshi Unno and
Yuki Satake and
Tachio Terauchi Relatively complete refinement type
system for verification of higher-order
non-deterministic programs . . . . . . . 12:1--12:??
Lionel Parreaux and
Antoine Voizard and
Amir Shaikhha and
Christoph E. Koch Unifying analytic and statically-typed
quasiquotes . . . . . . . . . . . . . . 13:1--13:??
Matt Brown and
Jens Palsberg Jones-optimal partial evaluation by
specialization-safe normalization . . . 14:1--14:??
John Peter Campora and
Sheng Chen and
Martin Erwig and
Eric Walkingshaw Migrating gradual types . . . . . . . . 15:1--15:??
Casper Bach Poulsen and
Arjen Rouvoet and
Andrew Tolmach and
Robbert Krebbers and
Eelco Visser Intrinsically-typed definitional
interpreters for imperative languages 16:1--16:??
Michalis Kokologiannakis and
Ori Lahav and
Konstantinos Sagonas and
Viktor Vafeiadis Effective stateless model checking for
C/C++ concurrency . . . . . . . . . . . 17:1--17:??
Brijesh Dongol and
Radha Jagadeesan and
James Riely Transactions in relaxed memory
architectures . . . . . . . . . . . . . 18:1--18:??
Christopher Pulte and
Shaked Flur and
Will Deacon and
Jon French and
Susmit Sarkar and
Peter Sewell Simplifying ARM concurrency:
multicopy-atomic axiomatic and
operational models for ARMv8 . . . . . . 19:1--19:??
Hongjin Liang and
Xinyu Feng Progress of concurrent objects with
partial methods . . . . . . . . . . . . 20:1--20:??
Thomas Williams and
Didier Rémy A principled approach to ornamentation
in ML . . . . . . . . . . . . . . . . . 21:1--21:??
William J. Bowman and
Youyou Cong and
Nick Rioux and
Amal Ahmed Type-preserving CPS translation of $
\Sigma $ and $ \Pi $ types is not not
possible . . . . . . . . . . . . . . . . 22:1--22:??
Andreas Abel and
Joakim Öhman and
Andrea Vezzosi Decidability of conversion for type
theory in type theory . . . . . . . . . 23:1--23:??
Ond\vrej Kun\vcar and
Andrei Popescu Safety and conservativity of definitions
in HOL and Isabelle/HOL . . . . . . . . 24:1--24:??
Michael Emmi and
Constantin Enea Sound, complete, and tractable
linearizability monitoring for
concurrent collections . . . . . . . . . 25:1--25:??
Oded Padon and
Jochen Hoenicke and
Giuliano Losa and
Andreas Podelski and
Mooly Sagiv and
Sharon Shoham Reducing liveness to safety in
first-order logic . . . . . . . . . . . 26:1--26:??
Gowtham Kaki and
Kartik Nagar and
Mahsa Najafzadeh and
Suresh Jagannathan Alone together: compositional reasoning
and inference for weak isolation . . . . 27:1--27:??
Ilya Sergey and
James R. Wilcox and
Zachary Tatlock Programming and proving with distributed
protocols . . . . . . . . . . . . . . . 28:1--28:??
Leandro T. C. Melo and
Rodrigo G. Ribeiro and
Marcus R. de Araújo and
Fernando Magno Quintão Pereira Inference of static semantics for
incomplete C programs . . . . . . . . . 29:1--29:??
Krishnendu Chatterjee and
Bhavya Choudhary and
Andreas Pavlogiannis Optimal Dyck reachability for
data-dependence and alias analysis . . . 30:1--30:??
Marek Chalupa and
Krishnendu Chatterjee and
Andreas Pavlogiannis and
Nishant Sinha and
Kapil Vaidya Data-centric dynamic partial order
reduction . . . . . . . . . . . . . . . 31:1--31:??
Wenlei Bao and
Sriram Krishnamoorthy and
Louis-Noel Pouchet and
P. Sadayappan Analytical modeling of cache behavior
for affine programs . . . . . . . . . . 32:1--32:??
Annabelle McIver and
Carroll Morgan and
Benjamin Lucien Kaminski and
Joost-Pieter Katoen A new proof rule for almost-sure
termination . . . . . . . . . . . . . . 33:1--33:??
Sheshansh Agrawal and
Krishnendu Chatterjee and
Petr Novotný Lexicographic ranking supermartingales:
an efficient approach to termination of
probabilistic programs . . . . . . . . . 34:1--34:??
Yangjia Li and
Mingsheng Ying Algorithmic analysis of termination
problems for quantum programs . . . . . 35:1--35:??
Ivan Radi\vcek and
Gilles Barthe and
Marco Gaboardi and
Deepak Garg and
Florian Zuleger Monadic refinements for relational cost
analysis . . . . . . . . . . . . . . . . 36:1--36:??
Siddharth Krishna and
Dennis Shasha and
Thomas Wies Go with the flow: compositional
abstractions for concurrent data
structures . . . . . . . . . . . . . . . 37:1--37:??
Dominique Devriese and
Marco Patrignani and
Frank Piessens Parametricity versus the universal type 38:1--38:??
Pierre Clairambault and
Charles Grellois and
Andrzej S. Murawski Linearity in higher-order recursion
schemes . . . . . . . . . . . . . . . . 39:1--39:??
Stephen Chang and
Alex Knauth and
Emina Torlak Symbolic types for lenient symbolic
execution . . . . . . . . . . . . . . . 40:1--40:??
Hsiang-Shang Ko and
Zhenjiang Hu An axiomatic basis for bidirectional
programming . . . . . . . . . . . . . . 41:1--41:??
Martin Odersky and
Olivier Blanvillain and
Fengyun Liu and
Aggelos Biboudis and
Heather Miller and
Sandro Stucki Simplicitly: foundations and
applications of implicit function types 42:1--42:??
Nils Anders Danielsson Up-to techniques using sized types . . . 43:1--43:??
Paolo Capriotti and
Nicolai Kraus Univalent higher categories via complete
Semi-Segal types . . . . . . . . . . . . 44:1--44:??
Leonidas Lampropoulos and
Zoe Paraskevopoulou and
Benjamin C. Pierce Generating good generators for inductive
relations . . . . . . . . . . . . . . . 45:1--45:??
Rupak Majumdar and
Filip Niksic Why is random testing effective for
partition tolerance bugs? . . . . . . . 46:1--46:??
Wonyeol Lee and
Rahul Sharma and
Alex Aiken On automatically proving the correctness
of math.h implementations . . . . . . . 47:1--47:??
Shelly Grossman and
Ittai Abraham and
Guy Golan-Gueta and
Yan Michalevsky and
Noam Rinetzky and
Mooly Sagiv and
Yoni Zohar Online detection of effectively callback
free objects with applications to smart
contracts . . . . . . . . . . . . . . . 48:1--48:??
Olivier Flückiger and
Gabriel Scherer and
Ming-Ho Yee and
Aviral Goel and
Amal Ahmed and
Jan Vitek Correctness of speculative optimizations
with dynamic deoptimization . . . . . . 49:1--49:??
José Fragoso Santos and
Petar Maksimovi\'c and
Daiva Naud\vzi\=unien\.e and
Thomas Wood and
Philippa Gardner JaVerT: JavaScript verification
toolchain . . . . . . . . . . . . . . . 50:1--50:??
Phúc C. Nguy\~ên and
Thomas Gilray and
Sam Tobin-Hochstadt and
David Van Horn Soft contract verification for
higher-order stateful programs . . . . . 51:1--51:??
Nada Amin and
Tiark Rompf Collapsing towers of interpreters . . . 52:1--52:??
Niki Vazou and
Anish Tondwalkar and
Vikraman Choudhury and
Ryan G. Scott and
Ryan R. Newton and
Philip Wadler and
Ranjit Jhala Refinement reflection: complete
verification with SMT . . . . . . . . . 53:1--53:??
Zachary Kincaid and
John Cyphert and
Jason Breck and
Thomas Reps Non-linear reasoning for invariant
synthesis . . . . . . . . . . . . . . . 54:1--54:??
Gagandeep Singh and
Markus Püschel and
Martin Vechev A practical construction for decomposing
numerical abstract domains . . . . . . . 55:1--55:??
Yuepeng Wang and
Isil Dillig and
Shuvendu K. Lahiri and
William R. Cook Verifying equivalence of database-driven
applications . . . . . . . . . . . . . . 56:1--56:??
Gilles Barthe and
Thomas Espitau and
Benjamin Grégoire and
Justin Hsu and
Pierre-Yves Strub Proving expected sensitivity of
probabilistic programs . . . . . . . . . 57:1--57:??
Aws Albarghouthi and
Justin Hsu Synthesizing coupling proofs of
differential privacy . . . . . . . . . . 58:1--58:??
Thomas Ehrhard and
Michele Pagani and
Christine Tasson Measurable cones and stable, measurable
functions: a model for probabilistic
higher-order programming . . . . . . . . 59:1--59:??
Adam \'Scibior and
Ohad Kammar and
Matthijs Vákár and
Sam Staton and
Hongseok Yang and
Yufei Cai and
Klaus Ostermann and
Sean K. Moss and
Chris Heunen and
Zoubin Ghahramani Denotational validation of higher-order
Bayesian inference . . . . . . . . . . . 60:1--60:??
Azadeh Farzan and
Zachary Kincaid Strategy synthesis for linear arithmetic
games . . . . . . . . . . . . . . . . . 61:1--61:??
Kartik Chandra and
Rastislav Bodik Bonsai: synthesis-based reasoning for
type systems . . . . . . . . . . . . . . 62:1--62:??
Xinyu Wang and
Isil Dillig and
Rishabh Singh Program synthesis using abstraction
refinement . . . . . . . . . . . . . . . 63:1--63:??
Amin Timany and
Léo Stefanesco and
Morten Krogh-Jespersen and
Lars Birkedal A logical relation for monadic
encapsulation of state: proving
contextual equivalences in the presence
of runST . . . . . . . . . . . . . . . . 64:1--64:??
Danel Ahman and
Cédric Fournet and
C\uat\ualin Hri\ctcu and
Kenji Maillard and
Aseem Rastogi and
Nikhil Swamy Recalling a witness: foundations and
applications of monotonic state . . . . 65:1--65:??
Ralf Jung and
Jacques-Henri Jourdan and
Robbert Krebbers and
Derek Dreyer RustBelt: securing the foundations of
the Rust programming language . . . . . 66:1--66:??
Oliver Bracevac and
Nada Amin and
Guido Salvaneschi and
Sebastian Erdweg and
Patrick Eugster and
Mira Mezini Versatile event correlation with
algebraic effects . . . . . . . . . . . 67:1--67:31
Jennifer Hackett and
Graham Hutton Parametric polymorphism and operational
improvement . . . . . . . . . . . . . . 68:1--68:24
Youyou Cong and
Kenichi Asai Handling delimited continuations with
dependent types . . . . . . . . . . . . 69:1--69:31
Conal Elliott The simple essence of automatic
differentiation . . . . . . . . . . . . 70:1--70:29
Ben Greenman and
Matthias Felleisen A spectrum of type soundness and
performance . . . . . . . . . . . . . . 71:1--71:32
Sven Keidel and
Casper Bach Poulsen and
Sebastian Erdweg Compositional soundness proofs of
abstract interpreters . . . . . . . . . 72:1--72:26
Max S. New and
Amal Ahmed Graduality from embedding-projection
pairs . . . . . . . . . . . . . . . . . 73:1--73:30
Rudi Horn and
Roly Perera and
James Cheney Incremental relational lenses . . . . . 74:1--74:30
Jesper Cockx and
Andreas Abel Elaborating dependent (co)pattern
matching . . . . . . . . . . . . . . . . 75:1--75:30
James Koppel and
Gabriel Scherer and
Armando Solar-Lezama Capturing the future by replaying the
past (functional pearl) . . . . . . . . 76:1--76:29
Robbert Krebbers and
Jacques-Henri Jourdan and
Ralf Jung and
Joseph Tassarotti and
Jan-Oliver Kaiser and
Amin Timany and
Arthur Charguéraud and
Derek Dreyer MoSeL: a general, extensible modal
framework for interactive proofs in
separation logic . . . . . . . . . . . . 77:1--77:30
Jan-Oliver Kaiser and
Beta Ziliani and
Robbert Krebbers and
Yann Régis-Gianas and
Derek Dreyer Mtac2: typed tactics for backward
reasoning in Coq . . . . . . . . . . . . 78:1--78:31
Andrey Mokhov and
Neil Mitchell and
Simon Peyton Jones Build systems \`a la carte . . . . . . . 79:1--79:29
Solomon Maina and
Anders Miltner and
Kathleen Fisher and
Benjamin C. Pierce and
David Walker and
Steve Zdancewic Synthesizing quotient lenses . . . . . . 80:1--80:29
Atsushi Ohori and
Katsuhiro Ueno and
Hisayuki Mima Finitary polymorphism for optimizing
type-directed compilation . . . . . . . 81:1--81:29
José Bacelar Almeida and
Alcino Cunha and
Nuno Macedo and
Hugo Pacheco and
José Proença Teaching how to program using automated
assessment and functional glossy games
(experience report) . . . . . . . . . . 82:1--82:17
Adam \'Scibior and
Ohad Kammar and
Zoubin Ghahramani Functional programming for modular
Bayesian inference . . . . . . . . . . . 83:1--83:29
Guillaume Boisseau and
Jeremy Gibbons What you needa know about Yoneda:
profunctor optics and the Yoneda lemma
(functional pearl) . . . . . . . . . . . 84:1--84:27
Csongor Kiss and
Matthew Pickering and
Nicolas Wu Generic deriving of generic traversals 85:1--85:30
Jeremy Gibbons and
Fritz Henglein and
Ralf Hinze and
Nicolas Wu Relational algebra by way of adjunctions 86:1--86:28
Mitchell Wand and
Ryan Culpepper and
Theophilos Giannakopoulos and
Andrew Cobb Contextual equivalence for a
probabilistic language with continuous
random variables and recursion . . . . . 87:1--87:30
Andrew K. Hirsch and
Ross Tate Strict and lazy semantics for effects:
layering monads and comonads . . . . . . 88:1--88:30
Joachim Breitner and
Antal Spector-Zabusky and
Yao Li and
Christine Rizkallah and
John Wiegley and
Stephanie Weirich Ready, set, verify! applying hs-to-coq
to real-world Haskell code (experience
report) . . . . . . . . . . . . . . . . 89:1--89:16
Guillaume Allais and
Robert Atkey and
James Chapman and
Conor McBride and
James McKinna A type and scope safe universe of
syntaxes with binding: their semantics
and proofs . . . . . . . . . . . . . . . 90:1--90:30
Ankush Das and
Jan Hoffmann and
Frank Pfenning Parallel complexity analysis with
temporal session types . . . . . . . . . 91:1--91:30
Nicolas Tabareau and
Éric Tanter and
Matthieu Sozeau Equivalences for free: univalent
parametricity for effective transport 92:1--92:29
Antonis Stampoulis and
Adam Chlipala Prototyping a functional language using
higher-order logic programming: a
functional pearl on learning the ways of
$ \lambda $ Prolog Makam . . . . . . . . 93:1--93:30
Beniamino Accattoli and
Stéphane Graham-Lengrand and
Delia Kesner Tight typings and split bounds . . . . . 94:1--94:30
Stefan K. Muller and
Umut A. Acar and
Robert Harper Competitive parallelism: getting your
priorities right . . . . . . . . . . . . 95:1--95:30
Ivan Perez Fault tolerant functional reactive
programming (functional pearl) . . . . . 96:1--96:30
Martin Elsman and
Troels Henriksen and
Danil Annenkov and
Cosmin E. Oancea Static interpretation of higher-order
modules in Futhark: functional GPU
programming in the large . . . . . . . . 97:1--97:30
John Peter Campora and
Sheng Chen and
Eric Walkingshaw Casts and costs: harmonizing safety and
performance in gradual typing . . . . . 98:1--98:30
Chandrakana Nandi and
James R. Wilcox and
Pavel Panchekha and
Taylor Blau and
Dan Grossman and
Zachary Tatlock Functional programming for compiling and
decompiling computer-aided design . . . 99:1--99:31
Jeremy Yallop and
Tamara von Glehn and
Ohad Kammar Partially-static data as free extension
of algebras . . . . . . . . . . . . . . 100:1--100:30
Brent A. Yorgey and
Kenneth Foner What's the difference? A functional
pearl on subtracting bijections . . . . 101:1--101:21
Kenneth Foner and
Hengchu Zhang and
Leonidas Lampropoulos Keep your laziness in check . . . . . . 102:1--102:30
Frédéric Bour and
Thomas Refis and
Gabriel Scherer Merlin: a language server for OCaml
(experience report) . . . . . . . . . . 103:1--103:15
Larry Diehl and
Denis Firsov and
Aaron Stump Generic zero-cost reuse for dependent
types . . . . . . . . . . . . . . . . . 104:1--104:30
Guannan Wei and
James Decker and
Tiark Rompf Refunctionalization of abstract abstract
machines: bridging the gap between
abstract abstract machines and abstract
definitional interpreters (functional
pearl) . . . . . . . . . . . . . . . . . 105:1--105:28
Cyrus Omar and
Jonathan Aldrich Reasonably programmable literal notation 106:1--106:32
Joscha Drechsler and
Ragnar Mogk and
Guido Salvaneschi and
Mira Mezini Thread-safe reactive programming . . . . 107:1--107:30
Benoit Daloze and
Arie Tal and
Stefan Marr and
Hanspeter Mössenböck and
Erez Petrank Parallelization of dynamic languages:
synchronizing built-in collections . . . 108:1--108:30
Remigius Meier and
Armin Rigo and
Thomas R. Gross Virtual machine design for parallel
dynamic programming languages . . . . . 109:1--109:25
Charith Mendis and
Saman Amarasinghe goSLP: globally optimized superword
level parallelism framework . . . . . . 110:1--110:28
Jonathan Immanuel Brachthäuser and
Philipp Schuster and
Klaus Ostermann Effect handlers for the masses . . . . . 111:1--111:27
Fabian Muehlboeck and
Ross Tate Empowering union and intersection types
with integrated subtyping . . . . . . . 112:1--112:29
Francesco Zappa Nardelli and
Julia Belyakova and
Artem Pelenitsyn and
Benjamin Chung and
Jeff Bezanson and
Jan Vitek Julia subtyping: a rational
reconstruction . . . . . . . . . . . . . 113:1--113:27
Hendrik van Antwerpen and
Casper Bach Poulsen and
Arjen Rouvoet and
Eelco Visser Scopes as types . . . . . . . . . . . . 114:1--114:30
Peixuan Li and
Danfeng Zhang A derivation framework for dependent
security label inference . . . . . . . . 115:1--115:26
Neville Grech and
Michael Kong and
Anton Jurisevic and
Lexi Brent and
Bernhard Scholz and
Yannis Smaragdakis MadMax: surviving out-of-gas conditions
in Ethereum smart contracts . . . . . . 116:1--116:27
Chu-Pan Wong and
Jens Meinicke and
Lukas Lazarek and
Christian Kästner Faster variational execution with
transparent bytecode transformation . . 117:1--117:30
Kalev Alpernas and
Cormac Flanagan and
Sadjad Fouladi and
Leonid Ryzhyk and
Mooly Sagiv and
Thomas Schmitz and
Keith Winstein Secure serverless computing using
dynamic information flow control . . . . 118:1--118:26
Roland Leißa and
Klaas Boesche and
Sebastian Hack and
Ars\`ene Pérard-Gayot and
Richard Membarth and
Philipp Slusallek and
André Müller and
Bertil Schmidt AnyDSL: a partial evaluation framework
for programming high-performance
libraries . . . . . . . . . . . . . . . 119:1--119:30
Jeff Bezanson and
Jiahao Chen and
Benjamin Chung and
Stefan Karpinski and
Viral B. Shah and
Jan Vitek and
Lionel Zoubritzky Julia: dynamism and performance
reconciled by design . . . . . . . . . . 120:1--120:23
Yunming Zhang and
Mengjiao Yang and
Riyadh Baghdadi and
Shoaib Kamil and
Julian Shun and
Saman Amarasinghe GraphIt: a high-performance graph DSL 121:1--121:30
James Koppel and
Varot Premtoon and
Armando Solar-Lezama One tool, many languages:
language-parametric transformation with
incremental parametric syntax . . . . . 122:1--122:28
Stephen Chou and
Fredrik Kjolstad and
Saman Amarasinghe Format abstraction for sparse tensor
algebra compilers . . . . . . . . . . . 123:1--123:30
Xiaoran Xu and
Keith Cooper and
Jacob Brock and
Yan Zhang and
Handong Ye ShareJIT: JIT code cache sharing across
processes and its practical
implementation . . . . . . . . . . . . . 124:1--124:23
Juneyoung Lee and
Chung-Kil Hur and
Ralf Jung and
Zhengyang Liu and
John Regehr and
Nuno P. Lopes Reconciling high-level optimizations and
low-level code in LLVM . . . . . . . . . 125:1--125:28
Zhangxiaowen Gong and
Zhi Chen and
Justin Szaday and
David Wong and
Zehra Sura and
Neftali Watkinson and
Saeed Maleki and
David Padua and
Alexander Veidenbaum and
Alexandru Nicolau and
Josep Torrellas An empirical study of the effect of
source-level loop transformations on
compiler stability . . . . . . . . . . . 126:1--126:29
Mikaël Mayer and
Viktor Kuncak and
Ravi Chugh Bidirectional evaluation with direct
manipulation . . . . . . . . . . . . . . 127:1--127:28
Jason Ott and
Tyson Loveless and
Chris Curtis and
Mohsen Lesani and
Philip Brisk BioScript: programming safe chemistry on
laboratories-on-a-chip . . . . . . . . . 128:1--128:31
Pascal Weisenburger and
Mirko Köhler and
Guido Salvaneschi Distributed system development with
ScalaLoci . . . . . . . . . . . . . . . 129:1--129:30
Michael Faes and
Thomas R. Gross Concurrency-aware object-oriented
programming with roles . . . . . . . . . 130:1--130:30
P. Ezudheen and
Daniel Neider and
Deepak D'Souza and
Pranav Garg and
P. Madhusudan Horn-ICE learning for synthesizing
invariants and contracts . . . . . . . . 131:1--131:25
Niki Vazou and
Éric Tanter and
David Van Horn Gradual liquid type inference . . . . . 132:1--132:25
Daniel Feltey and
Ben Greenman and
Christophe Scholliers and
Robert Bruce Findler and
Vincent St-Amour Collapsible contracts: fixing a
pathology of gradual typing . . . . . . 133:1--133:27
Jack Williams and
J. Garrett Morris and
Philip Wadler The root cause of blame: contracts for
intersection and union types . . . . . . 134:1--134:29
Parosh Aziz Abdulla and
Mohamed Faouzi Atig and
Bengt Jonsson and
Tuan Phong Ngo Optimal stateless model checking under
the release-acquire semantics . . . . . 135:1--135:29
Peizhao Ou and
Brian Demsky Towards understanding the costs of
avoiding out-of-thin-air results . . . . 136:1--136:29
Azalea Raad and
Viktor Vafeiadis Persistence semantics for weak memory:
integrating epoch persistency with the
TSO memory model . . . . . . . . . . . . 137:1--137:27
Jyothi Vedurada and
V. Krishna Nandivada Identifying refactoring opportunities
for replacing type code with subclass
and state . . . . . . . . . . . . . . . 138:1--138:28
Tamás Szabó and
Gábor Bergmann and
Sebastian Erdweg and
Markus Voelter Incrementalizing lattice-based program
analyses in Datalog . . . . . . . . . . 139:1--139:29
Minseok Jeon and
Sehun Jeong and
Hakjoo Oh Precise and scalable points-to analysis
via data-driven context tunneling . . . 140:1--140:29
Yue Li and
Tian Tan and
Anders Mòller and
Yannis Smaragdakis Precision-guided context sensitivity for
pointer analysis . . . . . . . . . . . . 141:1--141:29
Girish Maskeri Rama and
Raghavan Komondoor and
Himanshu Sharma Refinement in object-sensitivity
points-to analysis via slicing . . . . . 142:1--142:27
Nachshon Cohen Every data structure deserves lock-free
memory reclamation . . . . . . . . . . . 143:1--143:24
Sam Blackshear and
Nikos Gorogiannis and
Peter W. O'Hearn and
Ilya Sergey RacerD: compositional static race
detection . . . . . . . . . . . . . . . 144:1--144:28
Umang Mathur and
Dileep Kini and
Mahesh Viswanathan What happens --- after the first race?
Enhancing the predictive power of
happens-before based dynamic race
detection . . . . . . . . . . . . . . . 145:1--145:29
Christian Gram Kalhauge and
Jens Palsberg Sound deadlock prediction . . . . . . . 146:1--146:29
Michael Pradel and
Koushik Sen DeepBugs: a learning approach to
name-based bug detection . . . . . . . . 147:1--147:25
Daniel W. Barowy and
Emery D. Berger and
Benjamin Zorn ExceLint: automatically finding
spreadsheet formula errors . . . . . . . 148:1--148:26
James Bornholt and
Emina Torlak Finding code that explodes under
symbolic evaluation . . . . . . . . . . 149:1--149:26
Saswat Padhi and
Prateek Jain and
Daniel Perelman and
Oleksandr Polozov and
Sumit Gulwani and
Todd Millstein FlashProfile: a framework for
synthesizing data profiles . . . . . . . 150:1--150:28
Ulan Degenbaev and
Jochen Eisinger and
Kentaro Hara and
Marcel Hlopko and
Michael Lippautz and
Hannes Payer Cross-component garbage collection . . . 151:1--151:24
Sebastian Burckhardt and
Tim Coppieters Reactive caching for composed services:
polling at the speed of push . . . . . . 152:1--152:28
Nachshon Cohen and
David T. Aksun and
James R. Larus Object-oriented recovery for
non-volatile memory . . . . . . . . . . 153:1--153:22
Will Dietz and
Vikram Adve Software multiplexing: share your
libraries and statically link them too 154:1--154:26
Yuepeng Wang and
Xinyu Wang and
Isil Dillig Relational program synthesis . . . . . . 155:1--155:27
Pavol Bielik and
Marc Fischer and
Martin Vechev Robust relational layout synthesis from
examples for Android . . . . . . . . . . 156:1--156:29
Chenglong Wang and
Alvin Cheung and
Rastislav Bodik Speeding up symbolic reasoning for
relational queries . . . . . . . . . . . 157:1--157:25
Junho Lee and
Dowon Song and
Sunbeom So and
Hakjoo Oh Automatic diagnosis and correction of
logical errors for functional
programming assignments . . . . . . . . 158:1--158:30
Ankush Desai and
Amar Phanishayee and
Shaz Qadeer and
Sanjit A. Seshia Compositional programming and testing of
dynamic distributed systems . . . . . . 159:1--159:30
Burcu Kulahcioglu Ozkan and
Rupak Majumdar and
Filip Niksic and
Mitra Tabaei Befrouei and
Georg Weissenbacher Randomized testing of distributed
systems with probabilistic guarantees 160:1--160:28
Marija Selakovic and
Michael Pradel and
Rezwana Karim and
Frank Tip Test generation for higher-order
functions in dynamic languages . . . . . 161:1--161:27
Saba Alimadadi and
Di Zhong and
Magnus Madsen and
Frank Tip Finding broken promises in asynchronous
JavaScript programs . . . . . . . . . . 162:1--162:26
Brett Boston and
Zoe Gong and
Michael Carbin Leto: verifying application-specific
hardware fault tolerance with
programmable execution models . . . . . 163:1--163:30
Gowtham Kaki and
Kapil Earanky and
KC Sivaramakrishnan and
Suresh Jagannathan Safe replication through bounded
concurrency verification . . . . . . . . 164:1--164:27
Marcelo Sousa and
Isil Dillig and
Shuvendu K. Lahiri Verified three-way program merge . . . . 165:1--165:29
Fengmin Zhu and
Fei He Conflict resolution for structured merge
via version space algebra . . . . . . . 166:1--166:25
Evan Cavallo and
Robert Harper Higher inductive types in cubical
computational type theory . . . . . . . 1:1--1:27
Ambrus Kaposi and
András Kovács and
Thorsten Altenkirch Constructing quotient
inductive-inductive types . . . . . . . 2:1--2:24
Gaëtan Gilbert and
Jesper Cockx and
Matthieu Sozeau and
Nicolas Tabareau Definitional proof-irrelevance without K 3:1--3:28
Rasmus Ejlers Mògelberg and
Niccol\`o Veltri Bisimulation as path type for guarded
recursive types . . . . . . . . . . . . 4:1--4:29
Yizhou Zhang and
Andrew C. Myers Abstraction-safe effect handlers via
tunneling . . . . . . . . . . . . . . . 5:1--5:29
Dariusz Biernacki and
Maciej Piróg and
Piotr Polesiuk and
Filip Sieczkowski Abstracting algebraic effects . . . . . 6:1--6:28
Ugo Dal Lago and
Marc de Visme and
Damiano Mazza and
Akira Yoshimizu Intersection types and runtime errors in
the pi-calculus . . . . . . . . . . . . 7:1--7:29
Andrej Dudenhefner and
Jakob Rehof Principality and approximation under
dimensional bound . . . . . . . . . . . 8:1--8:29
Joshua Dunfield and
Neelakantan R. Krishnaswami Sound and complete bidirectional
typechecking for higher-rank
polymorphism with existentials and
indexed types . . . . . . . . . . . . . 9:1--9:28
Karl Crary Fully abstract module compilation . . . 10:1--10:29
Gyunghee Park and
Jaemin Hong and
Guy L. Steele Jr. and
Sukyoung Ryu Polymorphic symmetric multiple dispatch
with variance . . . . . . . . . . . . . 11:1--11:28
J. Garrett Morris and
James McKinna Abstracting extensible data types: or,
rows by any other name . . . . . . . . . 12:1--12:28
Di Wang and
Jan Hoffmann Type-guided worst-case input generation 13:1--13:30
Cyrus Omar and
Ian Voysey and
Ravi Chugh and
Matthew A. Hammer Live functional programming with typed
holes . . . . . . . . . . . . . . . . . 14:1--14:32
Max S. New and
Daniel R. Licata and
Amal Ahmed Gradual type theory . . . . . . . . . . 15:1--15:31
Giuseppe Castagna and
Victor Lanvin and
Tommaso Petrucciani and
Jeremy G. Siek Gradual typing: a new perspective . . . 16:1--16:32
Matías Toro and
Elizabeth Labrada and
Éric Tanter Gradual parametricity, revisited . . . . 17:1--17:30
Yusuke Miyazaki and
Taro Sekiyama and
Atsushi Igarashi Dynamic type inference for gradual
Hindley--Milner typing . . . . . . . . . 18:1--18:29
Lau Skorstengaard and
Dominique Devriese and
Lars Birkedal StkTokens: enforcing well-bracketed
control flow and stack encapsulation
using linear capabilities . . . . . . . 19:1--19:28
G. A. Kavvos Modalities, cohesion, and information
flow . . . . . . . . . . . . . . . . . . 20:1--20:29
Tom Hirschowitz Familial monads and structural
operational semantics . . . . . . . . . 21:1--21:28
Jasmin Christian Blanchette and
Lorenzo Gheri and
Andrei Popescu and
Dmitriy Traytel Bindings as bounded natural functors . . 22:1--22:34
Paul-André Mellies Categorical combinatorics of scheduling
and synchronization in game semantics 23:1--23:30
Wen Kokke and
Fabrizio Montesi and
Marco Peressotti Better late than never: a fully-abstract
semantics for classical processes . . . 24:1--24:29
Filippo Bonchi and
Joshua Holland and
Robin Piedeleu and
Pawe\l Soboci\'nski and
Fabio Zanasi Diagrammatic algebra: from linear to
concurrent systems . . . . . . . . . . . 25:1--25:28
Paolo Baldan and
Barbara König and
Christina Mika-Michalski and
Tommaso Padoan Fixpoint games on continuous lattices 26:1--26:29
Simon Castellan and
Nobuko Yoshida Two sides of the same coin: session
types and game semantics: a synchronous
side and an asynchronous side . . . . . 27:1--27:29
Simon Fowler and
Sam Lindley and
J. Garrett Morris and
Sára Decova Exceptional asynchronous session types:
session types without tiers . . . . . . 28:1--28:29
David Castro and
Raymond Hu and
Sung-Shik Jongmans and
Nicholas Ng and
Nobuko Yoshida Distributed programming using
role-parametric session types in Go:
statically-typed endpoint APIs for
dynamically-instantiated communication
structures . . . . . . . . . . . . . . . 29:1--29:30
Alceste Scalas and
Nobuko Yoshida Less is more: multiparty session types
revisited . . . . . . . . . . . . . . . 30:1--30:29
Matthew Flatt and
Caner Derici and
R. Kent Dybvig and
Andrew W. Keep and
Gustavo E. Massaccesi and
Sarah Spall and
Sam Tobin-Hochstadt and
Jon Zeppieri Rebuilding Racket on Chez Scheme
(experience report) . . . . . . . . . . 78:1--78:15
Youyou Cong and
Leo Osvald and
Grégory M. Essertel and
Tiark Rompf Compiling with continuations, or
without? Whatever . . . . . . . . . . . 79:1--79:28
Akimasa Morihata Lambda calculus with algebraic
simplification for reduction
parallelization by equational reasoning 80:1--80:25
Stefan K. Muller and
Sam Westrick and
Umut A. Acar Fairness in responsive parallelism . . . 81:1--81:30
Benjamin Delaware and
Sorawit Suriyakarn and
Clément Pit-Claudel and
Qianchuan Ye and
Adam Chlipala Narcissus: correct-by-construction
derivation of decoders and encoders from
binary formats . . . . . . . . . . . . . 82:1--82:29
Zoe Paraskevopoulou and
Andrew W. Appel Closure conversion is safe for space . . 83:1--83:29
Thomas Van Strydonck and
Frank Piessens and
Dominique Devriese Linear capabilities for fully abstract
compilation of separation-logic-verified
code . . . . . . . . . . . . . . . . . . 84:1--84:29
Daniel Patterson and
Amal Ahmed The next 700 compiler correctness
theorems (functional pearl) . . . . . . 85:1--85:29
Matthieu Sozeau and
Cyprien Mangin Equations reloaded: high-level
dependently-typed functional programming
and proving in Coq . . . . . . . . . . . 86:1--86:29
Andrea Vezzosi and
Anders Mörtberg and
Andreas Abel Cubical Agda: a dependently typed
programming language with univalence and
higher inductive types . . . . . . . . . 87:1--87:29
Joseph Eremondi and
Éric Tanter and
Ronald Garcia Approximate normalization for gradual
dependent types . . . . . . . . . . . . 88:1--88:30
Maximilian Algehed and
Jean-Philippe Bernardy Simple noninterference from
parametricity . . . . . . . . . . . . . 89:1--89:22
Andrey Mokhov and
Georgy Lukyanov and
Simon Marlow and
Jeremie Dimino Selective applicative functors . . . . . 90:1--90:29
Gert-Jan Bottu and
Ningning Xie and
Koar Marntirosian and
Tom Schrijvers Coherence of type class resolution . . . 91:1--91:28
Weihao Qu and
Marco Gaboardi and
Deepak Garg Relational cost analysis for
functional-imperative programs . . . . . 92:1--92:29
Hengchu Zhang and
Edo Roth and
Andreas Haeberlen and
Benjamin C. Pierce and
Aaron Roth Fuzzi: a three-level logic for
differential privacy . . . . . . . . . . 93:1--93:28
Calvin Smith and
Aws Albarghouthi Synthesizing differentially private
programs . . . . . . . . . . . . . . . . 94:1--94:29
Anders Miltner and
Solomon Maina and
Kathleen Fisher and
Benjamin C. Pierce and
David Walker and
Steve Zdancewic Synthesizing symmetric lenses . . . . . 95:1--95:28
Fei Wang and
Daniel Zheng and
James Decker and
Xilun Wu and
Grégory M. Essertel and
Tiark Rompf Demystifying differentiable programming:
shift/reset the penultimate
backpropagator . . . . . . . . . . . . . 96:1--96:31
Amir Shaikhha and
Andrew Fitzgibbon and
Dimitrios Vytiniotis and
Simon Peyton Jones Efficient differentiable programming in
a functional array-processing language 97:1--97:30
Rajan Walia and
Praveen Narayanan and
Jacques Carette and
Sam Tobin-Hochstadt and
Chung-chieh Shan From high-level inference algorithms to
efficient code . . . . . . . . . . . . . 98:1--98:30
Benjamin Sherman and
Jesse Michel and
Michael Carbin Sound and robust solid modeling via
exact real arithmetic and continuity . . 99:1--99:29
David Thrane Christiansen and
Iavor S. Diatchki and
Robert Dockins and
Joe Hendrix and
Tristan Ravitch Dependently typed Haskell in industry
(experience report) . . . . . . . . . . 100:1--100:16
Stephanie Weirich and
Pritam Choudhury and
Antoine Voizard and
Richard A. Eisenberg A role for dependent types in Haskell 101:1--101:29
Csongor Kiss and
Tony Field and
Susan Eisenbach and
Simon Peyton Jones Higher-order type-level programming in
Haskell . . . . . . . . . . . . . . . . 102:1--102:26
Wouter Swierstra and
Tim Baanen A predicate transformer semantics for
effects (functional pearl) . . . . . . . 103:1--103:26
Kenji Maillard and
Danel Ahman and
Robert Atkey and
Guido Martínez and
C\uat\ualin Hri\ctcu and
Exequiel Rivas and
Éric Tanter Dijkstra monads for all . . . . . . . . 104:1--104:29
Amin Timany and
Lars Birkedal Mechanized relational verification of
concurrent programs with continuations 105:1--105:28
Nicholas V. Lewchenko and
Arjun Radhakrishna and
Akash Gaonkar and
Pavol Cerný Sequential programming for replicated
data stores . . . . . . . . . . . . . . 106:1--106:28
Daniel Gratzer and
Jonathan Sterling and
Lars Birkedal Implementing a modal dependent type
theory . . . . . . . . . . . . . . . . . 107:1--107:29
Pierre-Marie Pédrot and
Nicolas Tabareau and
Hans Jacob Fehrmann and
Éric Tanter A reasonably exceptional type theory . . 108:1--108:29
Patrick Bahr and
Christian Uldal Graulund and
Rasmus Ejlers Mògelberg Simply RaTT: a fitch-style modal
calculus for reactive programming
without space leaks . . . . . . . . . . 109:1--109:27
Dominic Orchard and
Vilem-Benjamin Liepelt and
Harley Eades III Quantitative program reasoning with
graded modal types . . . . . . . . . . . 110:1--110:30
Bert Lindenhovius and
Michael Mislove and
Vladimir Zamdzhiev Mixed linear and non-linear recursive
types . . . . . . . . . . . . . . . . . 111:1--111:29
Jinxu Zhao and
Bruno C. d. S. Oliveira and
Tom Schrijvers A mechanical formalization of
higher-ranked polymorphic type inference 112:1--112:29
Victor Cacciari Miraldo and
Wouter Swierstra An efficient algorithm for type-safe
structural diffing . . . . . . . . . . . 113:1--113:29
Jennifer Hackett and
Graham Hutton Call-by-need is clairvoyant
call-by-value . . . . . . . . . . . . . 114:1--114:23
Aliya Hameer and
Brigitte Pientka Teaching the art of functional
programming using automated grading
(experience report) . . . . . . . . . . 115:1--115:15
Jeremy Yallop and
Leo White Lambda: the ultimate sublanguage
(experience report) . . . . . . . . . . 116:1--116:17
Kia Rahmani and
Kartik Nagar and
Benjamin Delaware and
Suresh Jagannathan CLOTHO: directed test generation for
weakly consistent database systems . . . 117:1--117:28
Osbert Bastani and
Xin Zhang and
Armando Solar-Lezama Probabilistic verification of fairness
properties via concentration . . . . . . 118:1--118:27
Vimuth Fernando and
Keyur Joshi and
Sasa Misailovic Verifying safety and accuracy of
approximate parallel programs via
canonical sequentialization . . . . . . 119:1--119:29
Marcos Yukio Siraichi and
Vinícius Fernandes dos Santos and
Caroline Collange and
Fernando Magno Quintão Pereira Qubit allocation as a combination of
subgraph isomorphism and token swapping 120:1--120:29
Arshavir Ter-Gabrielyan and
Alexander J. Summers and
Peter Müller Modular verification of heap
reachability properties in separation
logic . . . . . . . . . . . . . . . . . 121:1--121:28
Ben Greenman and
Matthias Felleisen and
Christos Dimoulas Complete monitors for gradual types . . 122:1--122:29
Igor Konnov and
Jure Kukovec and
Thanh-Hai Tran TLA+ model checking made symbolic . . . 123:1--123:30
Krishnendu Chatterjee and
Andreas Pavlogiannis and
Viktor Toman Value-centric dynamic partial order
reduction . . . . . . . . . . . . . . . 124:1--124:29
Ariya Shajii and
Ibrahim Numanagi\'c and
Riyadh Baghdadi and
Bonnie Berger and
Saman Amarasinghe Seq: a high-performance language for
bioinformatics . . . . . . . . . . . . . 125:1--125:29
Guannan Wei and
Yuxuan Chen and
Tiark Rompf Staged abstract interpreters: fast and
modular whole-program analysis via
meta-programming . . . . . . . . . . . . 126:1--126:32
Ian Henriksen and
Gianfranco Bilardi and
Keshav Pingali Derivative grammars: a symbolic approach
to parsing with derivatives . . . . . . 127:1--127:28
Yoav Zuriel and
Michal Friedman and
Gali Sheffi and
Nachshon Cohen and
Erez Petrank Efficient lock-free durable sets . . . . 128:1--128:26
Mingzhang Huang and
Hongfei Fu and
Krishnendu Chatterjee and
Amir Kafshdar Goharshady Modular verification for almost-sure
termination of probabilistic programs 129:1--129:29
Yu-Ping Wang and
Xu-Qiang Hu and
Zi-Xin Zou and
Wende Tan and
Gang Tan IVT: an efficient method for sharing
subtype polymorphic objects . . . . . . 130:1--130:22
Luís Caires and
Bernardo Toninho Refinement kinds: type-safe programming
with practical type-level computation 131:1--131:30
Benjamin Mariano and
Josh Reese and
Siyuan Xu and
ThanhVu Nguyen and
Xiaokang Qiu and
Jeffrey S. Foster and
Armando Solar-Lezama Program synthesis with algebraic library
specifications . . . . . . . . . . . . . 132:1--132:25
Conrad Watt and
Andreas Rossberg and
Jean Pichon-Pharabod Weakening WebAssembly . . . . . . . . . 133:1--133:28
Tetsuro Yamazaki and
Tomoki Nakamaru and
Kazuhiro Ichikawa and
Shigeru Chiba Generating a fluent API with syntax
checking from an LR grammar . . . . . . 134:1--134:24
Azalea Raad and
John Wickerson and
Viktor Vafeiadis Weak persistency semantics from the
ground up: formalising the persistency
semantics of ARMv8 and transactional
models . . . . . . . . . . . . . . . . . 135:1--135:27
Vilhelm Sjöberg and
Yuyang Sang and
Shu-chun Weng and
Zhong Shao DeepSEA: a language for certified system
software . . . . . . . . . . . . . . . . 136:1--136:27
Zhuo Zhang and
Wei You and
Guanhong Tao and
Guannan Wei and
Yonghwi Kwon and
Xiangyu Zhang BDA: practical dependence analysis for
binary executables by unbiased
whole-program path sampling and per-path
abstract interpretation . . . . . . . . 137:1--137:31
Ivana Vukotic and
Vincent Rahli and
Paulo Esteves-Veríssimo Asphalion: trustworthy shielding against
Byzantine faults . . . . . . . . . . . . 138:1--138:32
Rong Pan and
Qinheping Hu and
Gaowei Xu and
Loris D'Antoni Automatic repair of regular expressions 139:1--139:29
Benno Stein and
Benjamin Barslev Nielsen and
Bor-Yuh Evan Chang and
Anders Mòller Static analysis with demand-driven value
refinement . . . . . . . . . . . . . . . 140:1--140:29
Jia Chen and
Jiayi Wei and
Yu Feng and
Osbert Bastani and
Isil Dillig Relational verification using
reinforcement learning . . . . . . . . . 141:1--141:30
John Bender and
Jens Palsberg A formalization of Java's concurrent
access modes . . . . . . . . . . . . . . 142:1--142:28
Anders Miltner and
Sumit Gulwani and
Vu Le and
Alan Leung and
Arjun Radhakrishna and
Gustavo Soares and
Ashish Tiwari and
Abhishek Udupa On the fly synthesis of edit suggestions 143:1--143:29
Ragnar Mogk and
Joscha Drechsler and
Guido Salvaneschi and
Mira Mezini A fault-tolerant programming model for
distributed interactive applications . . 144:1--144:29
Marianna Rapoport and
Ondrej Lhoták A path to DOT: formalizing fully
path-dependent types . . . . . . . . . . 145:1--145:29
Théophile Bastian and
Stephen Kell and
Francesco Zappa Nardelli Reliable and fast DWARF-based stack
unwinding . . . . . . . . . . . . . . . 146:1--146:24
Vytautas Astrauskas and
Peter Müller and
Federico Poli and
Alexander J. Summers Leveraging Rust types for modular
specification and verification . . . . . 147:1--147:30
Jingbo Lu and
Jingling Xue Precision-preserving yet fast
object-sensitive pointer analysis with
partial context sensitivity . . . . . . 148:1--148:29
Abhinav Jangda and
Donald Pinckney and
Yuriy Brun and
Arjun Guha Formal foundations of serverless
computing . . . . . . . . . . . . . . . 149:1--149:26
Parosh Aziz Abdulla and
Mohamed Faouzi Atig and
Bengt Jonsson and
Magnus Lång and
Tuan Phong Ngo and
Konstantinos Sagonas Optimal stateless model checking for
reads-from equivalence under sequential
consistency . . . . . . . . . . . . . . 150:1--150:29
Pavel Panchekha and
Michael D. Ernst and
Zachary Tatlock and
Shoaib Kamil Modular verification of web page layout 151:1--151:26
Sifei Luan and
Di Yang and
Celeste Barnaby and
Koushik Sen and
Satish Chandra Aroma: code recommendation via
structural code search . . . . . . . . . 152:1--152:28
Aviral Goel and
Jan Vitek On the design, implementation, and use
of laziness in R . . . . . . . . . . . . 153:1--153:27
Gowtham Kaki and
Swarn Priya and
KC Sivaramakrishnan and
Suresh Jagannathan Mergeable replicated data types . . . . 154:1--154:29
Michaël Marcozzi and
Qiyi Tang and
Alastair F. Donaldson and
Cristian Cadar Compiler fuzzing: how much does it
matter? . . . . . . . . . . . . . . . . 155:1--155:29
Zachary Benavides and
Keval Vora and
Rajiv Gupta DProf: distributed profiler with strong
guarantees . . . . . . . . . . . . . . . 156:1--156:24
Grégory M. Essertel and
Guannan Wei and
Tiark Rompf Precise reasoning with structured time,
structured heaps, and collective
operations . . . . . . . . . . . . . . . 157:1--157:30
Luis Mastrangelo and
Matthias Hauswirth and
Nathaniel Nystrom Casting about in the dark: an empirical
study of cast operations in Java
programs . . . . . . . . . . . . . . . . 158:1--158:31
Johannes Bader and
Andrew Scott and
Michael Pradel and
Satish Chandra Getafix: learning to fix bugs
automatically . . . . . . . . . . . . . 159:1--159:27
Baijun Wu and
John Peter Campora III and
Yi He and
Alexander Schlecht and
Sheng Chen Generating precise error specifications
for C: a zero shot learning approach . . 160:1--160:30
Aleksandar Nanevski and
Anindya Banerjee and
Germán Andrés Delbianco and
Ignacio Fábregas Specifying concurrent programs in
separation logic: morphisms and
simulations . . . . . . . . . . . . . . 161:1--161:30
Yi Li and
Shaohua Wang and
Tien N. Nguyen and
Son Van Nguyen Improving bug detection via
context-based code representation
learning and attention-based neural
networks . . . . . . . . . . . . . . . . 162:1--162:30
Filip Krikava and
Heather Miller and
Jan Vitek Scala implicits are everywhere: a
large-scale study of the use of Scala
implicits in the wild . . . . . . . . . 163:1--163:28
Rajkishore Barik and
Manu Sridharan and
Murali Krishna Ramanathan and
Milind Chabbi Optimization of swift protocols . . . . 164:1--164:27
Ranadeep Biswas and
Constantin Enea On the complexity of checking
transactional consistency . . . . . . . 165:1--165:28
Jad Hamza and
Nicolas Voirol and
Viktor Kuncak System FR: formalized foundations for
the Stainless verifier . . . . . . . . . 166:1--166:30
Guido Salvaneschi and
Mirko Köhler and
Daniel Sokolowski and
Philipp Haller and
Sebastian Erdweg and
Mira Mezini Language-integrated privacy-aware
distributed queries . . . . . . . . . . 167:1--167:30
Rohan Bavishi and
Caroline Lemieux and
Roy Fox and
Koushik Sen and
Ion Stoica AutoPandas: neural-backed generators for
program synthesis . . . . . . . . . . . 168:1--168:27
Ulf Adams Ry\=u revisited: \tt printf floating
point conversion . . . . . . . . . . . . 169:1--169:23
Bo Shen and
Wei Zhang and
Haiyan Zhao and
Guangtai Liang and
Zhi Jin and
Qianxiang Wang IntelliMerge: a refactoring-aware
software merging technique . . . . . . . 170:1--170:28
Shengyi Wang and
Qinxiang Cao and
Anshuman Mohan and
Aquinas Hobor Certifying graph-manipulating C programs
via localizations within data structures 171:1--171:30
Joseph P. Near and
David Darais and
Chike Abuah and
Tim Stevens and
Pranav Gaddamadugu and
Lun Wang and
Neel Somani and
Mu Zhang and
Nikhil Sharma and
Alex Shan and
Dawn Song Duet: an expressive higher-order
language and linear type system for
statically enforcing differential
privacy . . . . . . . . . . . . . . . . 172:1--172:30
Michalis Kokologiannakis and
Azalea Raad and
Viktor Vafeiadis Effective lock handling in stateless
model checking . . . . . . . . . . . . . 173:1--173:26
Rohan Padhye and
Caroline Lemieux and
Koushik Sen and
Laurent Simon and
Hayawardh Vijayakumar FuzzFactory: domain-specific fuzzing
with waypoints . . . . . . . . . . . . . 174:1--174:29
José P. Cambronero and
Martin C. Rinard AL: autogenerating supervised learning
programs . . . . . . . . . . . . . . . . 175:1--175:28
Sven Keidel and
Sebastian Erdweg Sound and reusable components for
abstract interpretation . . . . . . . . 176:1--176:28
Ahmet Celik and
Pengyu Nie and
Christopher J. Rossbach and
Milos Gligoric Design, implementation, and application
of GPU-based Java bytecode interpreters 177:1--177:28
Timos Antonopoulos and
Eric Koskinen and
Ton Chanh Le Specification and inference of trace
refinement relations . . . . . . . . . . 178:1--178:30
Kaan Genç and
Jake Roemer and
Yufan Xu and
Michael D. Bond Dependence-aware, unbounded sound
predictive race detection . . . . . . . 179:1--179:30
Burcu Kulahcioglu Ozkan and
Rupak Majumdar and
Simin Oraee Trace aware random testing for
distributed systems . . . . . . . . . . 180:1--180:29
Leonidas Lampropoulos and
Michael Hicks and
Benjamin C. Pierce Coverage guided, property based testing 181:1--181:29
Emma Tosch and
Eytan Bakshy and
Emery D. Berger and
David D. Jensen and
J. Eliot B. Moss PlanAlyzer: assessing threats to the
validity of online experiments . . . . . 182:1--182:30
Milijana Surbatovich and
Limin Jia and
Brandon Lucia I/O dependent idempotence bugs in
intermittent systems . . . . . . . . . . 183:1--183:31
Christian Wimmer and
Codrut Stancu and
Peter Hofer and
Vojin Jovanovic and
Paul Wögerer and
Peter B. Kessler and
Oleg Pliss and
Thomas Würthinger Initialize once, start fast: application
initialization at build time . . . . . . 184:1--184:29
Ilya Sergey and
Vaivaswatha Nagaraj and
Jacob Johannsen and
Amrit Kumar and
Anton Trunov and
Ken Chan Guan Hao Safer smart contract programming with
Scilla . . . . . . . . . . . . . . . . . 185:1--185:30
Hashim Sharif and
Prakalp Srivastava and
Muhammad Huzaifa and
Maria Kotsifakou and
Keyur Joshi and
Yasmin Sarita and
Nathan Zhao and
Vikram S. Adve and
Sasa Misailovic and
Sarita Adve ApproxHPVM: a portable compiler IR for
accuracy-aware optimizations . . . . . . 186:1--186:30
August Shi and
Milica Hadzi-Tanovic and
Lingming Zhang and
Darko Marinov and
Owolabi Legunsen Reflection-aware static regression test
selection . . . . . . . . . . . . . . . 187:1--187:29
Dowon Song and
Myungho Lee and
Hakjoo Oh Automatic and scalable detection of
logical errors in functional programming
assignments . . . . . . . . . . . . . . 188:1--188:30
Shuai Wang and
Chengyu Zhang and
Zhendong Su Detecting nondeterministic payment bugs
in Ethereum smart contracts . . . . . . 189:1--189:29
Davide Barbarossa and
Giulio Manzonetto Taylor subsumes Scott, Berry, Kahn and
Plotkin . . . . . . . . . . . . . . . . 1:1--1:23
Martin Clochard and
Claude Marché and
Andrei Paskevich Deductive verification with ghost
monitors . . . . . . . . . . . . . . . . 2:1--2:26
Stephen Chang and
Michael Ballantyne and
Milo Turner and
William J. Bowman Dependent type systems as macros . . . . 3:1--3:29
Kenji Maillard and
Catalin Hritcu and
Exequiel Rivas and
Antoine Van Muylder The next 700 relational program logics 4:1--4:33
Yotam M. Y. Feldman and
Neil Immerman and
Mooly Sagiv and
Sharon Shoham Complexity and information in invariant
inference . . . . . . . . . . . . . . . 5:1--5:29
Jonas Kastberg Hinrichsen and
Jesper Bengtson and
Robbert Krebbers Actris: session-type based reasoning in
separation logic . . . . . . . . . . . . 6:1--6:30
Gilles Barthe and
Sandrine Blazy and
Benjamin Grégoire and
Rémi Hutin and
Vincent Laporte and
David Pichardie and
Alix Trieu Formal verification of a constant-time
preserving C compiler . . . . . . . . . 7:1--7:30
Matthieu Sozeau and
Simon Boulier and
Yannick Forster and
Nicolas Tabareau and
Théo Winterhalter Coq Coq correct! Verification of type
checking and erasure for Coq, in Coq . . 8:1--8:28
Jason Z. S. Hu and
Ondrej Lhoták Undecidability of $ d_\lt $: and its
decidable fragments . . . . . . . . . . 9:1--9:30
Peter W. O'Hearn Incorrectness logic . . . . . . . . . . 10:1--10:32
Azalea Raad and
John Wickerson and
Gil Neiger and
Viktor Vafeiadis Persistency semantics of the Intel-x86
architecture . . . . . . . . . . . . . . 11:1--11:31
Zheng Guo and
Michael James and
David Justo and
Jiaxiao Zhou and
Ziteng Wang and
Ranjit Jhala and
Nadia Polikarpova Program synthesis by type-guided
abstraction refinement . . . . . . . . . 12:1--12:28
Azadeh Farzan and
Anthony Vandikas Reductions for safety proofs . . . . . . 13:1--13:28
Sung Kook Kim and
Arnaud J. Venet and
Aditya V. Thakur Deterministic parallel fixpoint
computation . . . . . . . . . . . . . . 14:1--14:33
G. A. Kavvos and
Edward Morehouse and
Daniel R. Licata and
Norman Danner Recurrence extraction for functional
programs through call-by-push-value . . 15:1--15:31
Wonyeol Lee and
Hangyeol Yu and
Xavier Rival and
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 and
Francesco A. Genco Par means parallel: multiplicative
linear logic proofs as concurrent
functional programs . . . . . . . . . . 18:1--18:28
Alexander K. Lew and
Marco F. Cusumano-Towner and
Benjamin Sherman and
Michael Carbin and
Vikash K. Mansinghka Trace types and denotational semantics
for sound programmable inference in
probabilistic languages . . . . . . . . 19:1--19:32
Mengqi Liu and
Lionel Rieg and
Zhong Shao and
Ronghui Gu and
David Costanzo and
Jung-Eun Kim and
Man-Ki Yoon Virtual timeline: a formal abstraction
for verifying preemptive schedulers with
temporal isolation . . . . . . . . . . . 20:1--20:31
Gilles Barthe and
Justin Hsu and
Mingsheng Ying and
Nengkun Yu and
Li Zhou Relational proofs for quantum programs 21:1--21:29
Michael Arntzenius and
Neel Krishnaswami Semina\"\ive evaluation for a
higher-order functional language . . . . 22:1--22:28
Youngju Song and
Minki Cho and
Dongjoo Kim and
Yonghyun Kim and
Jeehoon Kang and
Chung-Kil Hur CompCertM: CompCert with C-assembly
linking and lightweight modular
verification . . . . . . . . . . . . . . 23:1--23:31
Martin A. T. Handley and
Niki Vazou and
Graham Hutton Liquidate your assets: reasoning about
resource usage in liquid Haskell . . . . 24:1--24:27
Peixin Wang and
Hongfei Fu and
Krishnendu Chatterjee and
Yuxin Deng and
Ming Xu Proving expected sensitivity of
probabilistic programs with randomized
variable-dependent termination time . . 25:1--25:30
Parosh Aziz Abdulla and
Mohamed Faouzi Atig and
Rojin Rezvan Parameterized verification under TSO is
PSPACE-complete . . . . . . . . . . . . 26:1--26:29
Yannick Forster and
Fabian Kunze and
Marc Roth The weak call-by-value $ \lambda
$-calculus is reasonable for both time
and space . . . . . . . . . . . . . . . 27:1--27:23
Roberto Bruni and
Roberto Giacobazzi and
Roberta Gori and
Isabel Garcia-Contreras and
Dusko Pavlovic Abstract extensionality: on the
properties of incomplete abstract
interpretations . . . . . . . . . . . . 28:1--28:28
Zeina Migeed and
Jens Palsberg What is decidable about gradual types? 29:1--29:29
David Binder and
Julian Jabs and
Ingo Skupin and
Klaus Ostermann Decomposition diversity with symmetric
data and codata . . . . . . . . . . . . 30:1--30:28
Benedikt Ahrens and
André Hirschowitz and
Ambroise Lafont and
Marco Maggesi Reduction monads and their signatures 31:1--31:29
Michael Sammler and
Deepak Garg and
Derek Dreyer and
Tadeusz Litak The high-level benefits of low-level
sandboxing . . . . . . . . . . . . . . . 32:1--32:32
Paulo Emílio de Vilhena and
François Pottier and
Jacques-Henri Jourdan Spy game: verifying a local generic
solver in Iris . . . . . . . . . . . . . 33:1--33:28
Hoang-Hai Dang and
Jacques-Henri Jourdan and
Jan-Oliver Kaiser and
Derek Dreyer RustBelt meets relaxed memory . . . . . 34:1--34:29
Umang Mathur and
Adithya Murali and
Paul Krogmeier and
P. Madhusudan and
Mahesh Viswanathan Deciding memory safety for single-pass
heap-manipulating programs . . . . . . . 35:1--35:29
Feras A. Saad and
Cameron E. Freer and
Martin C. Rinard and
Vikash K. Mansinghka Optimal approximate sampling from
discrete probability distributions . . . 36:1--36:31
Marcel Hark and
Benjamin Lucien Kaminski and
Jürgen Giesl and
Joost-Pieter Katoen Aiming low is harder: induction for
lower bounds in probabilistic program
verification . . . . . . . . . . . . . . 37:1--37:28
Martín Abadi and
Gordon D. Plotkin A simple differentiable programming
language . . . . . . . . . . . . . . . . 38:1--38:28
Alexander Vandenbroucke and
Tom Schrijvers P$ \lambda \omega $NK: functional
probabilistic NetKAT . . . . . . . . . . 39:1--39:27
Mark P. Jones and
J. Garrett Morris and
Richard A. Eisenberg Partial type constructors: or, making ad
hoc datatypes less ad hoc . . . . . . . 40:1--40:28
Ralf Jung and
Hoang-Hai Dang and
Jeehoon Kang and
Derek Dreyer Stacked borrows: an aliasing model for
Rust . . . . . . . . . . . . . . . . . . 41:1--41:32
Ryan Beckett and
Aarti Gupta and
Ratul Mahajan and
David Walker Abstract interpretation of distributed
network control planes . . . . . . . . . 42:1--42:27
Michael Greenberg and
Austin J. Blatt Executable formal semantics for the
POSIX shell . . . . . . . . . . . . . . 43:1--43:30
Timothy Bourke and
Lélio Brun and
Marc Pouzet Mechanized semantics and verified
compilation for a dataflow synchronous
language with reset . . . . . . . . . . 44:1--44:29
Ralf Jung and
Rodolphe Lepigre and
Gaurav Parthasarathy and
Marianna Rapoport and
Amin Timany and
Derek Dreyer and
Bart Jacobs The future is ours: prophecy variables
in separation logic . . . . . . . . . . 45:1--45:32
Max S. New and
Dustin Jamner and
Amal Ahmed Graduality and parametricity: together
again for the first time . . . . . . . . 46:1--46:32
Sam Westrick and
Rohan Yadav and
Matthew Fluet and
Umut A. Acar Disentanglement in nested-parallel
programs . . . . . . . . . . . . . . . . 47:1--47:32
Dariusz Biernacki and
Maciej Piróg and
Piotr Polesiuk and
Filip Sieczkowski Binders by day, labels by night: effect
instances via lexically scoped handlers 48:1--48:29
Chenglong Wang and
Yu Feng and
Rastislav Bodik and
Alvin Cheung and
Isil Dillig Visualization by example . . . . . . . . 49:1--49:28
David Darais and
Ian Sweet and
Chang Liu and
Michael Hicks A language for probabilistically
oblivious computation . . . . . . . . . 50:1--50:31
Li-yao Xia and
Yannick Zakowski and
Paul He and
Chung-Kil Hur and
Gregory Malecha and
Benjamin C. Pierce and
Steve Zdancewic Interaction trees: representing
recursive and impure programs in Coq . . 51:1--51:32
Malavika Samak and
Deokhwan Kim and
Martin C. Rinard Synthesizing replacement classes . . . . 52:1--52:33
Ningning Xie and
Richard A. Eisenberg and
Bruno C. d. S. Oliveira Kind inference for datatypes . . . . . . 53:1--53:28
Suguman Bansal and
Kedar S. Namjoshi and
Yaniv Sa'ar Synthesis of coordination programs from
linear temporal specifications . . . . . 54:1--54:27
Gilles Barthe and
Justin Hsu and
Kevin Liao A probabilistic separation logic . . . . 55:1--55:30
Shengwei An and
Rishabh Singh and
Sasa Misailovic and
Roopsha Samanta Augmented example-based synthesis using
relational perturbation properties . . . 56:1--56:24
Fredrik Dahlqvist and
Dexter Kozen Semantics of higher-order probabilistic
programs with conditioning . . . . . . . 57:1--57:29
Pierre-Marie Pédrot and
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 and
Muhan Zeng and
Yingfei Xiong and
Zhoulai Fu and
Lu Zhang and
Zhendong Su Detecting floating-point errors via
atomic conditions . . . . . . . . . . . 60:1--60:27
Steffen Smolka and
Nate Foster and
Justin Hsu and
Tobias Kappé and
Dexter Kozen and
Alexandra Silva Guarded Kleene algebra with tests:
verification of uninterpreted programs
in nearly linear time . . . . . . . . . 61:1--61:28
Mukund Raghothaman and
Jonathan Mendelson and
David Zhao and
Mayur Naik and
Bernhard Scholz Provenance-guided synthesis of Datalog
programs . . . . . . . . . . . . . . . . 62:1--62:27
Pierre Clairambault and
Marc de Visme Full abstraction for the quantum
lambda-calculus . . . . . . . . . . . . 63:1--63:28
Alo\"\is Brunel and
Damiano Mazza and
Michele Pagani Backpropagation in the simply typed
lambda-calculus with linear negation . . 64:1--64:27
Lukas Lazarek and
Alexis King and
Samanvitha Sundar and
Robert Bruce Findler and
Christos Dimoulas Does blame shifting work? . . . . . . . 65:1--65:29
Julian Mackay and
Alex Potanin and
Jonathan Aldrich and
Lindsay Groves Decidable subtyping for path dependent
types . . . . . . . . . . . . . . . . . 66:1--66:27
Peter Thiemann and
Vasco T. Vasconcelos Label-dependent session types . . . . . 67:1--67:29
Roland Meyer and
Sebastian Wolff Pointer life cycle types for lock-free
data structures with memory reclamation 68:1--68:36
Roger K. W. Hui and
Morten J. 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 and
Bill Long and
Jon Steidel History of coarrays and SPMD parallelism
in Fortran . . . . . . . . . . . . . . . 72:1--72:30
Walter Bright and
Andrei Alexandrescu and
Michael Parker Origins of the D programming language 73:1--73:38
Stefan Monnier and
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 and
Brendan Eich JavaScript: the first 20 years . . . . . 77:1--77:189
Jeffrey Kodosky LabVIEW . . . . . . . . . . . . . . . . 78:1--78:54
Cynthia Solomon and
Brian Harvey and
Ken Kahn and
Henry Lieberman and
Mark L. Miller and
Artemis Papert and
Brian Silverman History of Logo . . . . . . . . . . . . 79:1--79:66
William D. Clinger and
Mitchell Wand Hygienic macro technology . . . . . . . 80:1--80:110
Cleve Moler and
Jack Little A history of MATLAB . . . . . . . . . . 81:1--81:67
Brad J. Cox and
Steve Naroff and
Hansen Hsu The origins of Objective-C at
PPI/Stepstone and its evolution at NeXT 82:1--82:74
Peter Van Roy and
Seif Haridi and
Christian Schulte and
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 and
Robert Harper and
John Reppy The history of Standard ML . . . . . . . 86:1--86:100
Peter Flake and
Phil Moorby and
Steve Golson and
Arturo Salz and
Simon Davidmann Verilog HDL and its ancestors and
descendants . . . . . . . . . . . . . . 87:1--87:90
Xiaohong Chen and
Grigore Rosu A general approach to define binders
using matching logic . . . . . . . . . . 88:1--88:32
Alejandro Serrano and
Jurriaan Hage and
Simon Peyton Jones and
Dimitrios Vytiniotis A quick look at impredicativity . . . . 89:1--89:29
Andreas Abel and
Jean-Philippe Bernardy A unified view of modalities in type
systems . . . . . . . . . . . . . . . . 90:1--90:28
Matús Tejiscák A dependently typed calculus with
pattern matching and erasure inference 91:1--91:29
Bastian Hagedorn and
Johannes Lenfers and
Thomas K\oehler and
Xueying Qin and
Sergei Gorlatch and
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 and
Jonathan Immanuel Brachthäuser and
Klaus Ostermann Compiling effect handlers in
capability-passing style . . . . . . . . 93:1--93:28
Matthew Weidner and
Heather Miller and
Christopher Meiklejohn Composing and decomposing op-based CRDTs
with semidirect products . . . . . . . . 94:1--94:27
Nick Rioux and
Steve Zdancewic Computation focusing . . . . . . . . . . 95:1--95:27
Glen Mével and
Jacques-Henri Jourdan and
François Pottier Cosmo: a concurrent separation logic for
multicore OCaml . . . . . . . . . . . . 96:1--96:29
Joseph W. Cutler and
Daniel R. Licata and
Norman Danner Denotational recurrence extraction for
amortized analysis . . . . . . . . . . . 97:1--97:29
Nandor Licker and
Timothy M. Jones Duplo: a framework for OCaml post-link
optimisation . . . . . . . . . . . . . . 98:1--98:29
Ningning Xie and
Jonathan Immanuel Brachthäuser and
Daniel Hillerström and
Philipp Schuster and
Daan Leijen Effect handlers, evidently . . . . . . . 99:1--99:29
Daniel Hillerström and
Sam Lindley and
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 and
Theodore Park and
Scott Smith and
Shiwei Weng Higher-order demand-driven symbolic
evaluation . . . . . . . . . . . . . . . 102:1--102:28
Gabriel Radanne and
Hannes Saffrich and
Peter Thiemann Kindly bent to free us . . . . . . . . . 103:1--103:29
Paul Downen and
Zena M. Ariola and
Simon Peyton Jones and
Richard A. Eisenberg Kinds are calling conventions . . . . . 104:1--104:29
Nadia Polikarpova and
Deian Stefan and
Jean Yang and
Shachar Itzhaky and
Travis Hance and
Armando Solar-Lezama Liquid information flow control . . . . 105:1--105:30
Tristan Knoth and
Di Wang and
Adam Reynolds and
Jan Hoffmann and
Nadia Polikarpova Liquid resource types . . . . . . . . . 106:1--106:29
Sebastian Graf and
Simon Peyton Jones and
Ryan G. Scott Lower your guards: a compositional
pattern-match coverage checker . . . . . 107:1--107:30
Pierce Darragh and
Michael D. Adams Parsing with zippers (functional pearl) 108:1--108:28
Justin Lubin and
Nick Collins and
Cyrus Omar and
Ravi Chugh Program sketching with live
bidirectional evaluation . . . . . . . . 109:1--109:29
Di Wang and
David M. Kahn and
Jan Hoffmann Raising expectations: automating
expected cost analysis with types . . . 110:1--110:31
Vikraman Choudhury and
Neel Krishnaswami Recovering purity with comonads and
capabilities . . . . . . . . . . . . . . 111:1--111:28
Timothée Haudebourg and
Thomas Genet and
Thomas Jensen Regular language type inference with
term rewriting . . . . . . . . . . . . . 112:1--112:29
KC Sivaramakrishnan and
Stephen Dolan and
Leo White and
Sadiq Jaffer and
Tom Kelly and
Anmol Sahoo and
Sudha Parimala and
Atul Dhiman and
Anil Madhavapeddy Retrofitting parallelism onto OCaml . . 113:1--113:30
Paolo G. Giarrusso and
Léo Stefanesco and
Amin Timany and
Lars Birkedal and
Robbert Krebbers Scala step-by-step: soundness for DOT
with step-indexed logical relations in
Iris . . . . . . . . . . . . . . . . . . 114:1--114:29
Daniel Selsam and
Simon Hudon and
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 and
Takeshi Tsukada and
Atsushi Igarashi Signature restriction for polymorphic
algebraic effects . . . . . . . . . . . 117:1--117:30
Kazutaka Matsuda and
Meng Wang Sparcl: a language for
partially-invertible computation . . . . 118:1--118:31
Beno\^\it Montagu and
Thomas Jensen Stable relations and abstract
interpretation of higher-order programs 119:1--119:30
Jamie Willis and
Nicolas Wu and
Matthew Pickering Staged selective parser combinators . . 120:1--120:30
Nikhil Swamy and
Aseem Rastogi and
Aymeric Fromherz and
Denis Merigoux and
Danel Ahman and
Guido Mart\'ìnez SteelCore: an extensible concurrent
separation logic for effectful
dependently typed programs . . . . . . . 121:1--121:30
Aaron Stump and
Christopher Jenkins and
Stephan Spahn and
Colin McDonald Strong functional pearl: Harper's
regular-expression matcher in Cedille 122:1--122:25
Jeremiah Griffin and
Mohsen Lesani and
Narges Shadab and
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
Magnus Madsen and
Ondrej Lhoták Fixpoints for the masses: programming
with first-class Datalog constraints . . 125:1--125:28
Jonathan Immanuel Brachthäuser and
Philipp Schuster and
Klaus Ostermann Effects as capabilities: effect handlers
and lightweight effect polymorphism . . 126:1--126:30
André Pacak and
Sebastian Erdweg and
Tamás Szabó A systematic approach to deriving
incremental type checkers . . . . . . . 127:1--127:28
Yotam M. Y. Feldman and
Artem Khyzha and
Constantin Enea and
Adam Morrison and
Aleksandar Nanevski and
Noam Rinetzky and
Sharon Shoham Proving highly-concurrent traversals
correct . . . . . . . . . . . . . . . . 128:1--128:29
Cyril Six and
Sylvain Boulmé and
David Monniaux Certified and efficient instruction
scheduling: application to interlocked
VLIW processors . . . . . . . . . . . . 129:1--129:29
Giulia Meuli and
Mathias Soeken and
Martin Roetteler and
Thomas Häner Enabling accuracy-aware quantum
compilers using symbolic resource
estimation . . . . . . . . . . . . . . . 130:1--130:26
Guilherme Vieira Leobas and
Fernando Magno Quintão Pereira Semiring optimizations: dynamic elision
of expressions with identity and
absorbing elements . . . . . . . . . . . 131:1--131:28
Michael Coblenz and
Jonathan Aldrich and
Brad A. Myers and
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 and
Torsten Hoefler and
Matthias Troyer Assertion-based optimization of Quantum
programs . . . . . . . . . . . . . . . . 133:1--133:20
Rupak Majumdar and
Nobuko Yoshida and
Damien Zufferey Multiparty motion coordination: from
choreographies to robotics programs . . 134:1--134:30
Shankara Pailoor and
Xinyu Wang and
Hovav Shacham and
Isil Dillig Automated policy synthesis for system
call sandboxing . . . . . . . . . . . . 135:1--135:26
Vytautas Astrauskas and
Christoph Matheja and
Federico Poli and
Peter Müller and
Alexander J. Summers How do programmers use unsafe Rust? . . 136:1--136:27
Yu Wang and
Ke Wang and
Fengjuan Gao and
Linzhang Wang Learning semantic program embeddings
with graph interval neural network . . . 137:1--137:27
Breanna Devore-McDonald and
Emery D. Berger Mossad: defeating software plagiarism
detection . . . . . . . . . . . . . . . 138:1--138:28
Yizhou Zhang and
Guido Salvaneschi and
Andrew C. Myers Handling bidirectional control flow . . 139:1--139:30
Steven Holtzen and
Guy Van den Broeck and
Todd Millstein Scaling exact inference for discrete
probabilistic programs . . . . . . . . . 140:1--140:31
Aaron Bembenek and
Michael Greenberg and
Stephen Chong Formulog: Datalog for SMT-based static
analysis . . . . . . . . . . . . . . . . 141:1--141:31
Tongtong Xiang and
Jeff Y. Luo and
Werner Dietl Precise inference of expressive units of
measurement types . . . . . . . . . . . 142:1--142:28
Hongyu Liu and
Sam Silvestro and
Xiangyu Zhang and
Jian Huang and
Tongping Liu WATCHER: in-situ failure diagnosis . . . 143:1--143:27
Thodoris Sotiropoulos and
Stefanos Chaliasos and
Dimitris Mitropoulos and
Diomidis Spinellis A model for detecting faults in build
specifications . . . . . . . . . . . . . 144:1--144:30
Sean Bartell and
Will Dietz and
Vikram S. Adve Guided linking: dynamic linking without
the costs . . . . . . . . . . . . . . . 145:1--145:29
Hamed Gorjiara and
Guoqing Harry Xu and
Brian Demsky Satune: synthesizing efficient SAT
encoders . . . . . . . . . . . . . . . . 146:1--146:32
Shengjian Guo and
Yueqi Chen and
Jiyong Yu and
Meng Wu and
Zhiqiang Zuo and
Peng Li and
Yueqiang Cheng and
Huibo Wang Exposing cache timing side-channel leaks
through out-of-order symbolic execution 147:1--147:32
Fangyi Zhou and
Francisco Ferreira and
Raymond Hu and
Rumyana Neykova and
Nobuko Yoshida Statically verified refinements for
multiparty protocols . . . . . . . . . . 148:1--148:30
Robert Griesemer and
Raymond Hu and
Wen Kokke and
Julien Lange and
Ian Lance Taylor and
Bernardo Toninho and
Philip Wadler and
Nobuko Yoshida Featherweight Go . . . . . . . . . . . . 149:1--149:29
Gushu Li and
Li Zhou and
Nengkun Yu and
Yufei Ding and
Mingsheng Ying and
Yuan Xie Projection-based runtime assertions for
testing and debugging quantum programs 150:1--150:29
Azalea Raad and
Ori Lahav and
Viktor Vafeiadis Persistent Owicki---Gries reasoning: a
program logic for reasoning about
persistent programs on Intel-x86 . . . . 151:1--151:28
Christoph Sprenger and
Tobias Klenze and
Marco Eilers and
Felix A. Wolf and
Peter Müller and
Martin Clochard and
David Basin Igloo: soundly linking compositional
refinement and separation logic for
distributed system verification . . . . 152:1--152:31
Konstantinos Kallas and
Filip Niksic and
Caleb Stanford and
Rajeev Alur DiffStream: differential output testing
for stream processing programs . . . . . 153:1--153:29
Magnus Madsen and
Jaco van de Pol Polymorphic types and effects with
Boolean unification . . . . . . . . . . 154:1--154:29
David Castro-Perez and
Nobuko Yoshida CAMP: cost-aware multiparty session
protocols . . . . . . . . . . . . . . . 155:1--155:30
Cormac Flanagan and
Stephen N. Freund The anchor verifier for blocking and
non-blocking concurrent software . . . . 156:1--156:29
Ramy Shahin and
Marsha Chechik Automatic and efficient
variability-aware lifting of functional
programs . . . . . . . . . . . . . . . . 157:1--157:27
Ryan Senanayake and
Changwan Hong and
Ziheng Wang and
Amalee Wilson and
Stephen Chou and
Shoaib Kamil and
Saman Amarasinghe and
Fredrik Kjolstad A sparse iteration space transformation
framework for sparse tensor algebra . . 158:1--158:30
Hila Peleg and
Roi Gabay and
Shachar Itzhaky and
Eran Yahav Programming with a read--eval--synth
loop . . . . . . . . . . . . . . . . . . 159:1--159:30
Umar Farooq and
Zhijia Zhao and
Manu Sridharan and
Iulian Neamtiu LiveDroid: identifying and preserving
mobile app state in volatile runtime
environments . . . . . . . . . . . . . . 160:1--160:30
Xiaohong Chen and
Minh-Thai Trinh and
Nishant Rodrigues and
Lucas Peña and
Grigore Rosu Towards a unified proof framework for
automated fixpoint reasoning using
matching logic . . . . . . . . . . . . . 161:1--161:29
Noam Yefet and
Uri Alon and
Eran Yahav Adversarial examples for models of code 162:1--162:30
Milijana Surbatovich and
Brandon Lucia and
Limin Jia Towards a formal foundation of
intermittent computing . . . . . . . . . 163:1--163:31
Guannan Wei and
Oliver Bracevac and
Shangyin Tan and
Tiark Rompf Compiling symbolic execution with
staging and algebraic effects . . . . . 164:1--164:33
Hengchu Zhang and
Edo Roth and
Andreas Haeberlen and
Benjamin C. Pierce and
Aaron Roth Testing differential privacy with dual
interpreters . . . . . . . . . . . . . . 165:1--165:26
Julie L. Newcomb and
Andrew Adams and
Steven Johnson and
Rastislav Bodik and
Shoaib Kamil Verifying and improving Halide's term
rewriting system with program synthesis 166:1--166:28
Gabriel Poesia and
Fernando Magno Quintão Pereira Dynamic dispatch of context-sensitive
optimizations . . . . . . . . . . . . . 167:1--167:28
Anders Mòller and
Oskar Haarklou Veileborg Eliminating abstraction overhead of Java
stream pipelines using ahead-of-time
program optimization . . . . . . . . . . 168:1--168:29
Sarah Spall and
Neil Mitchell and
Sam Tobin-Hochstadt Build scripts with perfect dependencies 169:1--169:28
John Feser and
Sam Madden and
Nan Tang and
Armando Solar-Lezama Deductive optimization of relational
data storage . . . . . . . . . . . . . . 170:1--170:30
Joshua Clune and
Vijay Ramamurthy and
Ruben Martins and
Umut A. Acar Program equivalence for assisted grading
of functional programs . . . . . . . . . 171:1--171:29
Martin Avanzini and
Georg Moser and
Michael Schaper A modular cost analysis for
probabilistic programs . . . . . . . . . 172:1--172:30
Dietrich Geisler and
Irene Yoon and
Aditi Kabra and
Horace He and
Yinnon Sanders and
Adrian Sampson Geometry types for graphics programming 173:1--173:25
Zhefeng Wu and
Zhe Sun and
Kai Gong and
Lingyun Chen and
Bin Liao and
Yihua Jin Hidden inheritance: an inline caching
design for TypeScript performance . . . 174:1--174:29
Fengyun Liu and
Ondrej Lhoták and
Aggelos Biboudis and
Paolo G. Giarrusso and
Martin Odersky A type-and-effect system for object
initialization . . . . . . . . . . . . . 175:1--175:28
Subarno Banerjee and
David Devecsery and
Peter M. Chen and
Satish Narayanasamy Sound garbage collection for C using
pointer provenance . . . . . . . . . . . 176:1--176:28
Manasij Mukherjee and
Pranav Kant and
Zhengyang Liu and
John Regehr Dataflow-based pruning for speeding up
superoptimization . . . . . . . . . . . 177:1--177:24
Ana Milanova FlowCFL: generalized type-based
reachability analysis: graph reduction
and equivalence of CFL-based and
type-based reachability . . . . . . . . 178:1--178:29
Minseok Jeon and
Myungho Lee and
Hakjoo Oh Learning graph-based heuristics for
pointer analysis without handcrafting
application-specific features . . . . . 179:1--179:30
Arjen Rouvoet and
Hendrik van Antwerpen and
Casper Bach Poulsen and
Robbert Krebbers and
Eelco Visser Knowing when to ask: sound scheduling of
name resolution in type checkers derived
from declarative specifications . . . . 180:1--180:28
Alexi Turcotte and
Aviral Goel and
Filip Krikava and
Jan Vitek Designing types for R, empirically . . . 181:1--181:25
Aayan Kumar and
Vivek Seshadri and
Rahul Sharma Shiftry: RNN inference in 2KB of RAM . . 182:1--182:30
Lingkun Kong and
Konstantinos Mamouras StreamQL: a query language for
processing streaming time series . . . . 183:1--183:32
Qianshan Yu and
Fei He and
Bow-Yaw Wang Incremental predicate analysis for
regression verification . . . . . . . . 184:1--184:25
Caterina Urban and
Maria Christakis and
Valentin Wüstholz and
Fuyuan Zhang Perfectly parallel fairness
certification of neural networks . . . . 185:1--185:30
Quentin Stiévenart and
Magnus Madsen Fuzzing channel-based concurrency
runtimes using types and effects . . . . 186:1--186:27
Anders Mòller and
Benjamin Barslev Nielsen and
Martin Toldam Torp Detecting locations in JavaScript
programs affected by breaking library
changes . . . . . . . . . . . . . . . . 187:1--187:25
Mirko Köhler and
Nafise Eskandani and
Pascal Weisenburger and
Alessandro Margara and
Guido Salvaneschi Rethinking safe consistency in
distributed object-oriented programming 188:1--188:30
Ton Chanh Le and
Timos Antonopoulos and
Parisa Fathololumi and
Eric Koskinen and
ThanhVu Nguyen DynamiTe: dynamic termination and
non-termination proofs . . . . . . . . . 189:1--189:30
Sifis Lagouvardos and
Neville Grech and
Ilias Tsatiris and
Yannis Smaragdakis Precise static modeling of Ethereum
``memory'' . . . . . . . . . . . . . . . 190:1--190:26
John Peter Campora and
Sheng Chen Taming type annotations in gradual
typing . . . . . . . . . . . . . . . . . 191:1--191:30
Minh-Thai Trinh and
Duc-Hiep Chu and
Joxan Jaffar Inter-theory dependency analysis for SMT
string solvers . . . . . . . . . . . . . 192:1--192:27
Dominik Winterer and
Chengyu Zhang and
Zhendong Su On the unusual effectiveness of
type-aware operator mutations for
testing SMT solvers . . . . . . . . . . 193:1--193:25
Radha Jagadeesan and
Alan Jeffrey and
James Riely Pomsets with preconditions: a simple
model of relaxed memory . . . . . . . . 194:1--194:30
Tobias Grosser and
Theodoros Theodoridis and
Maximilian Falkenstein and
Arjun Pitchanathan and
Michael Kruse and
Manuel Rigger and
Zhendong Su and
Torsten Hoefler Fast linear programming through
transprecision computing on small and
sparse data . . . . . . . . . . . . . . 195:1--195:28
Vsevolod Livinskii and
Dmitry Babokin and
John Regehr Random testing for C and C++ compilers
with YARPGen . . . . . . . . . . . . . . 196:1--196:25
Yuting Wang and
Xiangzhe Xu and
Pierre Wilke and
Zhong Shao CompCertELF: verified separate
compilation of C programs into ELF
object files . . . . . . . . . . . . . . 197:1--197:28
Bo Sang and
Patrick Eugster and
Gustavo Petri and
Srivatsan Ravi and
Pierre-Louis Roman Scalable and serializable networked
multi-actor programming . . . . . . . . 198:1--198:30
Fei He and
Jitao Han Termination analysis for evolving
programs: an incremental approach by
reusing certified modules . . . . . . . 199:1--199:27
Eric Atkinson and
Michael Carbin Programming and reasoning with partial
observability . . . . . . . . . . . . . 200:1--200:28
Ivan Gavran and
Eva Darulova and
Rupak Majumdar Interactive synthesis of temporal
specifications from examples and natural
language . . . . . . . . . . . . . . . . 201:1--201:26
Wing Lam and
Stefan Winter and
Anjiang Wei and
Tao Xie and
Darko Marinov and
Jonathan Bell A large-scale longitudinal study of
flaky tests . . . . . . . . . . . . . . 202:1--202:29
Hailong Zhang and
Yu Hao and
Sufian Latif and
Raef Bassily and
Atanas Rountev Differentially-private software
frequency profiling under linear
constraints . . . . . . . . . . . . . . 203:1--203:24
Alejandro Gómez-Londoño and
Johannes Åman Pohjola and
Hira Taqdees Syeda and
Magnus O. Myreen and
Yong Kiam Tan Do you have space for dessert? A
verified space cost semantics for CakeML
programs . . . . . . . . . . . . . . . . 204:1--204:29
Michael B. James and
Zheng Guo and
Ziteng Wang and
Shivani Doshi and
Hila Peleg and
Ranjit Jhala and
Nadia Polikarpova Digging for fold: synthesis-aided API
discovery for Haskell . . . . . . . . . 205:1--205:27
Koar Marntirosian and
Tom Schrijvers and
Bruno C. d. S. Oliveira and
Georgios Karachalias Resolution as intersection subtyping via
Modus Ponens . . . . . . . . . . . . . . 206:1--206:30
Julia Belyakova and
Benjamin Chung and
Jack Gelinas and
Jameson Nash and
Ross Tate and
Jan Vitek World age in Julia: optimizing method
dispatch in the presence of eval . . . . 207:1--207:26
Ifaz Kabir and
Yufeng Li and
Ondrej Lhoták $ \iota $DOT: a DOT calculus with object
initialization . . . . . . . . . . . . . 208:1--208:28
Elvira Albert and
Shelly Grossman and
Noam Rinetzky and
Clara Rodr\'ìguez-Núñez and
Albert Rubio and
Mooly Sagiv Taming callbacks for smart contract
modularity . . . . . . . . . . . . . . . 209:1--209:30
Cezara Dragoi and
Constantin Enea and
Burcu Kulahcioglu Ozkan and
Rupak Majumdar and
Filip Niksic Testing consensus implementations using
communication closure . . . . . . . . . 210:1--210:29
Manuel Rigger and
Zhendong Su Finding bugs in database systems via
query partitioning . . . . . . . . . . . 211:1--211:30
Sumit Gulwani and
Vu Le and
Arjun Radhakrishna and
Ivan Radicek and
Mohammad Raza Structure interpretation of text formats 212:1--212:29
Cezara Dragoi and
Josef Widder and
Damien Zufferey Programming at the edge of synchrony . . 213:1--213:30
Mehdi Bagherzadeh and
Nicholas Fireman and
Anas Shawesh and
Raffi Khatchadourian Actor concurrency bugs: a comprehensive
study on symptoms, root causes, API
usages, and differences . . . . . . . . 214:1--214:32
Shaked Brody and
Uri Alon and
Eran Yahav A structural model for contextual code
changes . . . . . . . . . . . . . . . . 215:1--215:28
Yiyun Liu and
James Parker and
Patrick Redmond and
Lindsey Kuper and
Michael Hicks and
Niki Vazou Verifying replicated data types with
typeclass refinements in Liquid Haskell 216:1--216:30
Pengyu Nie and
Marinela Parovic and
Zhiqiang Zang and
Sarfraz Khurshid and
Aleksandar Milicevic and
Milos Gligoric Unifying execution of imperative
generators and declarative
specifications . . . . . . . . . . . . . 217:1--217:26
Lenka Turo\vnová and
Luká\vs Hol\'ìk and
Ond\vrej Lengál and
Olli Saarikivi and
Margus Veanes and
Tomá\vs Vojnar Regex matching with counting-set
automata . . . . . . . . . . . . . . . . 218:1--218:30
Xiang Gao and
Shraddha Barke and
Arjun Radhakrishna and
Gustavo Soares and
Sumit Gulwani and
Alan Leung and
Nachiappan Nagappan and
Ashish Tiwari Feedback-driven semi-supervised
synthesis of program transformations . . 219:1--219:30
Olivier Flückiger and
Guido Chari and
Ming-Ho Yee and
Jan Jecmen and
Jakob Hain and
Jan Vitek Contextual dispatch for function
specialization . . . . . . . . . . . . . 220:1--220:24
Shubhani Gupta and
Abhishek Rose and
Sorav Bansal Counterexample-guided correlation
algorithm for translation validation . . 221:1--221:29
Leif Andersen and
Michael Ballantyne and
Matthias Felleisen Adding interactive visual syntax to
textual code . . . . . . . . . . . . . . 222:1--222:28
Yaoda Zhou and
Bruno C. d. S. Oliveira and
Jinxu Zhao Revisiting iso-recursive subtyping . . . 223:1--223:28
Ruyi Ji and
Yican Sun and
Yingfei Xiong and
Zhenjiang Hu Guiding dynamic programming via
structural probability for accelerating
programming by example . . . . . . . . . 224:1--224:29
Yaniv David and
Uri Alon and
Eran Yahav Neural reverse engineering of stripped
binaries using augmented control flow
graphs . . . . . . . . . . . . . . . . . 225:1--225:28
Jake Kirkham and
Tyler Sorensen and
Esin Tureci and
Margaret Martonosi Foundations of empirical memory
consistency testing . . . . . . . . . . 226:1--226:29
Shraddha Barke and
Hila Peleg and
Nadia Polikarpova Just-in-time learning for bottom-up
enumerative synthesis . . . . . . . . . 227:1--227:29
Jenna Wise and
Johannes Bader and
Cameron Wong and
Jonathan Aldrich and
Éric Tanter and
Joshua Sunshine Gradual verification of recursive heap
data structures . . . . . . . . . . . . 228:1--228:28
Michael Ballantyne and
Alexis King and
Matthias Felleisen Macros for domain-specific languages . . 229:1--229:29
Suvam Mukherjee and
Pantazis Deligiannis and
Arpita Biswas and
Akash Lal Learning-based controlled concurrency
testing . . . . . . . . . . . . . . . . 230:1--230:31
Emily First and
Yuriy Brun and
Arjun Guha TacTok: semantics-aware proof synthesis 231:1--231:31
Ritwika Ghosh and
Chiao Hsieh and
Sasa Misailovic and
Sayan Mitra Koord: a language for programming and
verifying distributed robotics
application . . . . . . . . . . . . . . 232:1--232:30
Yulei Sui and
Xiao Cheng and
Guanqin Zhang and
Haoyu Wang Flow2Vec: value-flow-based precise code
embedding . . . . . . . . . . . . . . . 233:1--233:27
Denis Kuperberg and
Laureline Pinault and
Damien Pous Cyclic proofs, system t, and the power
of contraction . . . . . . . . . . . . . 1:1--1:28
Patrick Bahr and
Christian Uldal Graulund and
Rasmus Ejlers Mògelberg Diamonds are not forever: liveness in
reactive programming with guarded
recursion . . . . . . . . . . . . . . . 2:1--2:28
Benjamin Sherman and
Jesse Michel and
Michael Carbin $ \lambda_s $: computable semantics for
differentiable programming with
higher-order functions and datatypes . . 3:1--3:31
Roy Margalit and
Ori Lahav Verifying observational robustness
against a C11-style memory model . . . . 4:1--4:33
Franti\vsek Farka and
Aleksandar Nanevski and
Anindya Banerjee and
Germán Andrés Delbianco and
Ignacio Fábregas On algebraic abstractions for concurrent
separation logics . . . . . . . . . . . 5:1--5:32
A\"\ina Linn Georges and
Armaël Guéneau and
Thomas Van Strydonck and
Amin Timany and
Alix Trieu and
Sander Huyghebaert and
Dominique Devriese and
Lars Birkedal Efficient and provable local capability
revocation using uninitialized
capabilities . . . . . . . . . . . . . . 6:1--6:30
Koen Jacobs and
Amin Timany and
Dominique Devriese Fully abstract from static to gradual 7:1--7:30
Gilles Barthe and
Rohit Chadha and
Paul Krogmeier and
A. Prasad Sistla and
Mahesh Viswanathan Deciding accuracy of differential
privacy schemes . . . . . . . . . . . . 8:1--8:30
Chao-Hong Chen and
Amr Sabry A computational interpretation of
compact closed categories: reversible
programming with negative and fractional
types . . . . . . . . . . . . . . . . . 9:1--9:29
Simon Oddershede Gregersen and
Johan Bay and
Amin Timany and
Lars Birkedal Mechanized logical relations for
termination-insensitive noninterference 10:1--10:29
Marcin Sabok and
Sam Staton and
Dario Stein and
Michael Wolman Probabilistic programming semantics for
name generation . . . . . . . . . . . . 11:1--11:29
Carlo Angiuli and
Evan Cavallo and
Anders Mörtberg and
Max Zeuner Internalizing representation
independence with univalence . . . . . . 12:1--12:30
Simon Spies and
Neel Krishnaswami and
Derek Dreyer Transfinite step-indexing for
termination . . . . . . . . . . . . . . 13:1--13:29
Michael Benedikt and
Pierre Pradic Generating collection transformations
from proofs . . . . . . . . . . . . . . 14:1--14:28
Yotam M. Y. Feldman and
Mooly Sagiv and
Sharon Shoham and
James R. Wilcox Learning the boundary of inductive
invariants . . . . . . . . . . . . . . . 15:1--15:30
Silvia Ghilezan and
Jovanka Pantovi\'c and
Ivan Proki\'c and
Alceste Scalas and
Nobuko Yoshida Precise subtyping for asynchronous
multiparty sessions . . . . . . . . . . 16:1--16:28
Kostas Ferles and
Jon Stephens and
Isil Dillig Verifying correct usage of context-free
API protocols . . . . . . . . . . . . . 17:1--17:30
Jatin Arora and
Sam Westrick and
Umut A. Acar Provably space-efficient parallel
functional programming . . . . . . . . . 18:1--18:33
Zvonimir Pavlinovic and
Yusen Su and
Thomas Wies Data flow refinement type inference . . 19:1--19:31
Cambridge Yang and
Eric Atkinson and
Michael Carbin Simplifying dependent reductions in the
polyhedral model . . . . . . . . . . . . 20:1--20:33
Marco Patrignani and
Eric Mark Martin and
Dominique Devriese On the semantic expressiveness of
recursive types . . . . . . . . . . . . 21:1--21:29
Arjen Rouvoet and
Robbert Krebbers and
Eelco Visser Intrinsically typed compilation with
nameless labels . . . . . . . . . . . . 22:1--22:28
Max Willsey and
Chandrakana Nandi and
Yisu Remy Wang and
Oliver Flatt and
Zachary Tatlock and
Pavel Panchekha egg: Fast and extensible equality
saturation . . . . . . . . . . . . . . . 23:1--23:29
Danel Ahman and
Matija Pretnar Asynchronous effects . . . . . . . . . . 24:1--24:28
Stefan K. Muller and
Jan Hoffmann Modeling and analyzing evaluation cost
of CUDA kernels . . . . . . . . . . . . 25:1--25:31
Lucas Silver and
Steve Zdancewic Dijkstra monads forever:
termination-sensitive specifications for
interaction trees . . . . . . . . . . . 26:1--26:28
Vineet Rajani and
Marco Gaboardi and
Deepak Garg and
Jan Hoffmann A unifying type-theory for higher-order
(amortized) cost analysis . . . . . . . 27:1--27:28
Damiano Mazza and
Michele Pagani Automatic differentiation in PCF . . . . 28:1--28:27
Jay P. Lim and
Mridul Aanjaneya and
John Gustafson and
Santosh Nagarakatte An approach to generate correctly
rounded math libraries for new floating
point variants . . . . . . . . . . . . . 29:1--29:30
Jinwoo Kim and
Qinheping Hu and
Loris D'Antoni and
Thomas Reps Semantics-guided synthesis . . . . . . . 30:1--30:32
Julian Rosemann and
Simon Moll and
Sebastian Hack An abstract interpretation for SPMD
divergence on reducible control flow
graphs . . . . . . . . . . . . . . . . . 31:1--31:31
Ugo Dal Lago and
Claudia Faggian and
Simona Ronchi Della Rocca Intersection types and (positive)
almost-sure termination . . . . . . . . 32:1--32:32
Paulo Emílio de Vilhena and
François Pottier A separation logic for effect handlers 33:1--33:28
Anders Alnor Mathiasen and
Andreas Pavlogiannis The fine-grained and parallel complexity
of Andersen's pointer analysis . . . . . 34:1--34:29
Andrew K. Hirsch and
Ethan Cecchetti Giving semantics to program-counter
labels via secure effects . . . . . . . 35:1--35:29
Umang Mathur and
Andreas Pavlogiannis and
Mahesh Viswanathan Optimal prediction of
synchronization-preserving races . . . . 36:1--36:29
Kesha Hietala and
Robert Rand and
Shih-Han Hung and
Xiaodi Wu and
Michael Hicks A verified optimizer for quantum
circuits . . . . . . . . . . . . . . . . 37:1--37:29
Jens Oliver Gutsfeld and
Markus Müller-Olm and
Christoph Ohrem Automata and fixpoints for asynchronous
hyperproperties . . . . . . . . . . . . 38:1--38:29
Kevin Batz and
Benjamin Lucien Kaminski and
Joost-Pieter Katoen and
Christoph Matheja Relatively complete verification of
probabilistic programs: an expressive
language for expectation-based reasoning 39:1--39:30
Nathanaël Courant and
Xavier Leroy Verified code generation for the
polyhedral model . . . . . . . . . . . . 40:1--40:24
Ryan Doenges and
Mina Tahmasbi Arashloo and
Santiago Bautista and
Alexander Chang and
Newton Ni and
Samwise Parkinson and
Rudy Peterson and
Alaia Solko-Breslin and
Amanda Xu and
Nate Foster Petr4: formal foundations for p4 data
planes . . . . . . . . . . . . . . . . . 41:1--41:32
Léon Gondelman and
Simon Oddershede Gregersen and
Abel Nieto and
Amin Timany and
Lars Birkedal Distributed causal memory: modular
specification and verification in
higher-order distributed separation
logic . . . . . . . . . . . . . . . . . 42:1--42:29
Michalis Kokologiannakis and
Ilya Kaysin and
Azalea Raad and
Viktor Vafeiadis PerSeVerE: persistency semantics for
verification under ext4 . . . . . . . . 43:1--43:29
Pascal Baumann and
Rupak Majumdar and
Ramanathan S. Thinniyam and
Georg Zetzsche Context-bounded verification of liveness
properties for multithreaded
shared-memory programs . . . . . . . . . 44:1--44:31
Alban Reynaud and
Gabriel Scherer and
Jeremy Yallop A practical mode system for recursive
definitions . . . . . . . . . . . . . . 45:1--45:29
Aur\`ele Barri\`ere and
Sandrine Blazy and
Olivier Flückiger and
David Pichardie and
Jan Vitek Formally verified speculation and
deoptimization in a JIT compiler . . . . 46:1--46:26
Artem Khyzha and
Ori Lahav Taming x86-TSO persistency . . . . . . . 47:1--47:29
Shaull Almagor and
Toghrul Karimov and
Edon Kelmendi and
Joël Ouaknine and
James Worrell Deciding $ \omega $-regular properties
on linear recurrence sequences . . . . . 48:1--48:24
Marco Vassena and
Craig Disselkoen and
Klaus von Gleissenthall and
Sunjay Cauligi and
Rami Gökhan Kìcì and
Ranjit Jhala and
Dean Tullsen and
Deian Stefan Automatically eliminating speculative
leaks from cryptographic code with Blade 49:1--49:30
Pritam Choudhury and
Harley Eades III and
Richard A. Eisenberg and
Stephanie Weirich A graded dependent type system with a
usage-aware semantics . . . . . . . . . 50:1--50:32
Beniamino Accattoli and
Ugo Dal Lago and
Gabriele Vanoni The (in)efficiency of interaction . . . 51:1--51:33
Alejandro Aguirre and
Gilles Barthe and
Justin Hsu and
Benjamin Lucien Kaminski and
Joost-Pieter Katoen and
Christoph Matheja A pre-expectation calculus for
probabilistic sensitivity . . . . . . . 52:1--52:28
Cameron Moy and
Phúc C. Nguy\~ên and
Sam Tobin-Hochstadt and
David Van Horn Corpse reviver: sound and efficient
gradual typing via contract verification 53:1--53:28
Woosuk Lee Combining the top-down propagation and
bottom-up enumeration for inductive
program synthesis . . . . . . . . . . . 54:1--54:28
Eddie Jones and
Steven Ramsay Intensional datatype refinement: with
application to scalable verification of
pattern-match safety . . . . . . . . . . 55:1--55:29
Parosh Aziz Abdulla and
Mohamed Faouzi Atig and
Ahmed Bouajjani and
K. Narayan Kumar and
Prakash Saivasan Deciding reachability under persistent
x86-TSO . . . . . . . . . . . . . . . . 56:1--56:32
Ivan Di Liberti and
Fosco Loregian and
Chad Nester and
Pawe\l Soboci\'nski Functorial semantics for partial
theories . . . . . . . . . . . . . . . . 57:1--57:28
Jules Jacobs Paradoxes of probabilistic programming:
and how to condition on events of
measure zero with infinitesimal
probabilities . . . . . . . . . . . . . 58:1--58:26
Yuanbo Li and
Qirun Zhang and
Thomas Reps On the complexity of bidirected
interleaved Dyck-reachability . . . . . 59:1--59:28
Jesper Cockx and
Nicolas Tabareau and
Théo Winterhalter The taming of the rew: a type theory
with computational assumptions . . . . . 60:1--60:29
Felipe Bañados Schwerter and
Alison M. Clark and
Khurram A. Jafery and
Ronald Garcia Abstracting gradual typing moving
forward: precise and space-efficient . . 61:1--61:28
Zesen Qian and
G. A. Kavvos and
Lars Birkedal Client-server sessions in linear logic 62:1--62:31
Nicolas Krauter and
Patrick Raaf and
Peter Braam and
Reza Salkhordeh and
Sebastian Erdweg and
André Brinkmann Persistent software transactional memory
in Haskell . . . . . . . . . . . . . . . 63:1--63:29
Richard A. Eisenberg and
Guillaume Duboc and
Stephanie Weirich and
Daniel Lee An existential crisis resolved: type
inference for first-class existential
types . . . . . . . . . . . . . . . . . 64:1--64:29
Shivam Handa and
Konstantinos Kallas and
Nikos Vasilakis and
Martin C. Rinard An order-aware dataflow model for
parallel Unix pipelines . . . . . . . . 65:1--65:28
Glen Mével and
Jacques-Henri Jourdan Formal verification of a concurrent
bounded queue in a weak memory model . . 66:1--66:29
Yannick Zakowski and
Calvin Beck and
Irene Yoon and
Ilia Zaichuk and
Vadim Zaliva and
Steve Zdancewic Modular, compositional, and executable
formal semantics for LLVM IR . . . . . . 67:1--67:30
Lukas Lazarek and
Ben Greenman and
Matthias Felleisen and
Christos Dimoulas How to evaluate blame for gradual types 68:1--68:29
Sandro Stucki and
Paolo G. Giarrusso A theory of higher-order subtyping with
type intervals . . . . . . . . . . . . . 69:1--69:30
Manuel Serrano Of JavaScript AOT compilation
performance . . . . . . . . . . . . . . 70:1--70:30
Ningning Xie and
Daan Leijen Generalized evidence passing for effect
handlers: efficient compilation of
effect handlers to C . . . . . . . . . . 71:1--71:30
Donnacha Oisín Kidney and
Nicolas Wu Algebras for weighted search . . . . . . 72:1--72:30
Zhixuan Yang and
Nicolas Wu Reasoning about effect interaction by
fusion . . . . . . . . . . . . . . . . . 73:1--73:29
John M. Li and
Andrew W. Appel Deriving efficient program
transformations from rewrite rules . . . 74:1--74:29
Nikita Zyuzin and
Aleksandar Nanevski Contextual modal types for algebraic
effects and handlers . . . . . . . . . . 75:1--75:29
David M. Kahn and
Jan Hoffmann Automatic amortized resource analysis
with the quantum physicist's method . . 76:1--76:29
Denis Merigoux and
Nicolas Chataing and
Jonathan Protzenko \pkgCatala: a programming language for
the law . . . . . . . . . . . . . . . . 77:1--77:29
Conal Elliott Symbolic and automatic differentiation
of languages . . . . . . . . . . . . . . 78:1--78:18
Pedro Rocha and
Luís Caires Propositions-as-types and shared state 79:1--79:30
Yao Li and
Li-yao Xia and
Stephanie Weirich Reasoning about the garden of forking
paths . . . . . . . . . . . . . . . . . 80:1--80:28
Lars Birkedal and
Thomas Dinsdale-Young and
Armaël Guéneau and
Guilhem Jaber and
Kasper Svendsen and
Nikos Tzevelekos Theorems for free from separation logic
specifications . . . . . . . . . . . . . 81:1--81:29
Mitchell Pickard and
Graham Hutton Calculating dependently-typed compilers
(functional pearl) . . . . . . . . . . . 82:1--82:27
Farzin Houshmand and
Mohsen Lesani and
Keval Vora \pkgGrafs: declarative graph analytics 83:1--83:32
Yasunari Watanabe and
Kiran Gopinathan and
George P\^\irlea and
Nadia Polikarpova and
Ilya Sergey Certifying the synthesis of
heap-manipulating programs . . . . . . . 84:1--84:29
Aymeric Fromherz and
Aseem Rastogi and
Nikhil Swamy and
Sydney Gibson and
Guido Martínez and
Denis Merigoux and
Tahina Ramananandro \pkgSteel: proof-oriented programming in
a dependently typed concurrent
separation logic . . . . . . . . . . . . 85:1--85:30
Zoe Paraskevopoulou and
John M. Li and
Andrew W. Appel Compositional optimizations for CertiCoq 86:1--86:30
Martin Avanzini and
Gilles Barthe and
Ugo Dal Lago On continuation-passing transformations
and expected cost analysis . . . . . . . 87:1--87:30
Adam Paszke and
Daniel D. Johnson and
David Duvenaud and
Dimitrios Vytiniotis and
Alexey Radul and
Matthew J. Johnson and
Jonathan Ragan-Kelley and
Dougal Maclaurin Getting to the point: index sets and
parallelism-preserving autodiff for
pointful array programming . . . . . . . 88:1--88:29
Xuejing Huang and
Bruno C. d. S. Oliveira Distributing intersection and union
types with splits and duality
(functional pearl) . . . . . . . . . . . 89:1--89:24
Nick Giannarakis and
Alexandra Silva and
David Walker \pkgProbNV: probabilistic verification
of network control planes . . . . . . . 90:1--90:30
Chaitanya Koparkar and
Mike Rainey and
Michael Vollmer and
Milind Kulkarni and
Ryan R. Newton Efficient tree-traversals: reconciling
parallelism and dense data
representations . . . . . . . . . . . . 91:1--91:29
Joshua Yanovski and
Hoang-Hai Dang and
Ralf Jung and
Derek Dreyer \pkgGhostCell: separating permissions
from data in Rust . . . . . . . . . . . 92:1--92:30
Alejandro Aguirre and
Gilles Barthe and
Marco Gaboardi and
Deepak Garg and
Shin-ya Katsumata and
Tetsuya Sato Higher-order probabilistic adversarial
computations: categorical semantics and
program logics . . . . . . . . . . . . . 93:1--93:30
Adam Chlipala Skipping the binder bureaucracy with
mixed embeddings in a semantics course
(functional pearl) . . . . . . . . . . . 94:1--94:28
Taro Sekiyama and
Takeshi Tsukada CPS transformation with affine types for
call-by-value implicit polymorphism . . 95:1--95:30
Kimball Germane and
Jay McCarthy Newly-single and loving it: improving
higher-order must-alias analysis with
heap fragments . . . . . . . . . . . . . 96:1--96:28
Wolf Honoré and
Jieung Kim and
Ji-Yong Shin and
Zhong Shao Much ADO about failures: a fault-aware
model for compositional verification of
strongly consistent distributed systems 97:1--97:31
Ori Lahav and
Egor Namakonov and
Jonas Oberhauser and
Anton Podkopaev and
Viktor Vafeiadis Making weak memory models fair . . . . . 98:1--98:27
Pengbo Yan and
Toby Murray \pkgSecRSL: security separation logic
for C11 release-acquire concurrency . . 99:1--99:26
Gust Verbruggen and
Vu Le and
Sumit Gulwani Semantic programming by example with
pre-trained models . . . . . . . . . . . 100:1--100:25
Aviral Goel and
Jan Jecmen and
Sebastián Krynski and
Olivier Flückiger and
Jan Vitek Promises are made to be broken:
migrating R to strict semantics . . . . 101:1--101:20
Georgios Karachalias and
Filip Koprivec and
Matija Pretnar and
Tom Schrijvers Efficient compilation of algebraic
effect handlers . . . . . . . . . . . . 102:1--102:28
Natalie Popescu and
Ziyang Xu and
Sotiris Apostolakis and
David I. August and
Amit Levy Safer at any speed: automatic
context-aware safety enhancement for
Rust . . . . . . . . . . . . . . . . . . 103:1--103:23
Angello Astorga and
Shambwaditya Saha and
Ahmad Dinkins and
Felicia Wang and
P. Madhusudan and
Tao Xie Synthesizing contracts correct modulo a
test generator . . . . . . . . . . . . . 104:1--104:27
Masaomi Yamaguchi and
Kazutaka Matsuda and
Cristina David and
Meng Wang \pkgSynbit: synthesizing bidirectional
programs using unidirectional sketches 105:1--105:31
Milod Kazerounian and
Jeffrey S. Foster and
Bonan Min \pkgSimTyper: sound type inference for
Ruby using type equality prediction . . 106:1--106:27
Kevin De Porre and
Carla Ferreira and
Nuno Preguiça and
Elisa Gonzalez Boix \pkgECROs: building global scale systems
from sequential code . . . . . . . . . . 107:1--107:30
Weili Fu and
Fabian Krause and
Peter Thiemann Label dependent lambda calculus and
gradual typing . . . . . . . . . . . . . 108:1--108:29
Luke Anderson and
Andrew Adams and
Karima Ma and
Tzu-Mao Li and
Tian Jin and
Jonathan Ragan-Kelley Efficient automatic scheduling of
imaging and vision pipelines for the GPU 109:1--109:28
Magnus Madsen and
Jaco van de Pol Relational nullable types with Boolean
unification . . . . . . . . . . . . . . 110:1--110:28
Luna Phipps-Costin and
Carolyn Jane Anderson and
Michael Greenberg and
Arjun Guha Solver-based gradual type migration . . 111:1--111:27
Guoqiang Zhang and
Yuanchao Xu and
Xipeng Shen and
Isil Dillig UDF to SQL translation through
compositional lazy inductive synthesis 112:1--112:26
Nisarg Patel and
Siddharth Krishna and
Dennis Shasha and
Thomas Wies Verifying concurrent multicopy search
structures . . . . . . . . . . . . . . . 113:1--113:32
Zoe Paraskevopoulou and
Anvay Grover Compiling with continuations, correctly 114:1--114:29
Eric Atkinson and
Guillaume Baudart and
Louis Mandel and
Charles Yuan and
Michael Carbin Statically bounded-memory delayed
sampling for probabilistic streams . . . 115:1--115:28
Zhe Zhou and
Robert Dickerson and
Benjamin Delaware and
Suresh Jagannathan Data-driven abductive inference of
library specifications . . . . . . . . . 116:1--116:29
Yann Herklotz and
James D. Pollard and
Nadesh Ramanathan and
John Wickerson Formal verification of high-level
synthesis . . . . . . . . . . . . . . . 117:1--117:30
Peisen Yao and
Qingkai Shi and
Heqing Huang and
Charles Zhang Program analysis via efficient symbolic
abstraction . . . . . . . . . . . . . . 118:1--118:32
Chandrakana Nandi and
Max Willsey and
Amy Zhu and
Yisu Remy Wang and
Brett Saiki and
Adam Anderson and
Adriana Schulz and
Dan Grossman and
Zachary Tatlock Rewrite rule inference using equality
saturation . . . . . . . . . . . . . . . 119:1--119:28
Dan Iorga and
Alastair F. Donaldson and
Tyler Sorensen and
John Wickerson The semantics of shared memory in Intel
CPU/FPGA systems . . . . . . . . . . . . 120:1--120:28
Mehmet Emre and
Ryan Schroeder and
Kyle Dewey and
Ben Hardekopf Translating C to safer Rust . . . . . . 121:1--121:29
Sándor Bartha and
James Cheney and
Vaishak Belle One down, 699 to go: or, synthesising
compositional desugarings . . . . . . . 122:1--122:29
Stefanos Chaliasos and
Thodoris Sotiropoulos and
Georgios-Petros Drosos and
Charalambos Mitropoulos and
Dimitris Mitropoulos and
Diomidis Spinellis Well-typed programs can go wrong: a
study of typing-related bugs in JVM
compilers . . . . . . . . . . . . . . . 123:1--123:30
Malte Viering and
Raymond Hu and
Patrick Eugster and
Lukasz Ziarek A multiparty session typing discipline
for fault-tolerant event-driven
distributed programming . . . . . . . . 124:1--124:30
Aviral Goel and
Pierre Donat-Bouillud and
Filip Krikava and
Christoph M. Kirsch and
Jan Vitek What we eval in the shadows: a
large-scale study of eval in R programs 125:1--125:23
Stefan Malewski and
Michael Greenberg and
Éric Tanter Gradually structured data . . . . . . . 126:1--126:29
Fabian Muehlboeck and
Ross Tate Transitioning from structural to nominal
code with efficient gradual typing . . . 127:1--127:29
Rawn Henry and
Olivia Hsu and
Rohan Yadav and
Stephen Chou and
Kunle Olukotun and
Saman Amarasinghe and
Fredrik Kjolstad Compilation of sparse array programming
models . . . . . . . . . . . . . . . . . 128:1--128:29
Robert Brotzman and
Danfeng Zhang and
Mahmut Taylan Kandemir and
Gang Tan \pkgSpecSafe: detecting cache side
channels in a speculative world . . . . 129:1--129:28
Xipeng Shen and
Guoqiang Zhang and
Irene Dea and
Samantha Andow and
Emilio Arroyo-Fang and
Neal Gafter and
Johann George and
Melissa Grueter and
Erik Meijer and
Olin Grigsby Shivers and
Steffi Stumpos and
Alanna Tempest and
Christy Warden and
Shannon Yang Coarsening optimization for
differentiable programming . . . . . . . 130:1--130:27
Tyler Sorensen and
Lucas F. Salvador and
Harmit Raval and
Hugues Evrard and
John Wickerson and
Margaret Martonosi and
Alastair F. Donaldson Specifying and testing GPU workgroup
progress models . . . . . . . . . . . . 131:1--131:30
Ranadeep Biswas and
Diptanshu Kakwani and
Jyothi Vedurada and
Constantin Enea and
Akash Lal \pkgMonkeyDB: effectively testing
correctness under weak isolation levels 132:1--132:27
Sebastian Burckhardt and
Chris Gillum and
David Justo and
Konstantinos Kallas and
Connor McMahon and
Christopher S. Meiklejohn Durable functions: semantics for
stateful serverless . . . . . . . . . . 133:1--133:27
Rohan Bavishi and
Caroline Lemieux and
Koushik Sen and
Ion Stoica \pkgGauss: program synthesis by
reasoning over graphs . . . . . . . . . 134:1--134:29
Paul He and
Eddy Westbrook and
Brent Carmer and
Chris Phifer and
Valentin Robert and
Karl Smeltzer and
Andrei \cStef\uanescu and
Aaron Tomb and
Adam Wick and
Matthew Yacavone and
Steve Zdancewic A type system for extracting functional
specifications from memory-safe
imperative programs . . . . . . . . . . 135:1--135:29
Haoran Xu and
Fredrik Kjolstad Copy-and-patch compilation: a fast
compilation algorithm for high-level
languages and bytecode . . . . . . . . . 136:1--136:30
Ori Roth Study of the subtyping machine of
nominal subtyping with variance . . . . 137:1--137:27
Didier Ishimwe and
KimHao Nguyen and
ThanhVu Nguyen \pkgDynaplex: analyzing program
complexity using dynamically inferred
recurrence relations . . . . . . . . . . 138:1--138:23
Yuyan Bao and
Guannan Wei and
Oliver Bracevac and
Yuxuan Jiang and
Qiyang He and
Tiark Rompf Reachability types: tracking aliasing
and separation in higher-order
functional programs . . . . . . . . . . 139:1--139:32
Jialu Zhang and
Ruzica Piskac and
Ennan Zhai and
Tianyin Xu Static detection of silent
misconfigurations with deep interaction
analysis . . . . . . . . . . . . . . . . 140:1--140:30
Ziqiao Zhou and
Michael K. Reiter Interpretable noninterference
measurement and its application to
processor designs . . . . . . . . . . . 141:1--141:30
Son Tuan Vu and
Albert Cohen and
Arnaud De Grandmaison and
Christophe Guillon and
Karine Heydemann Reconciling optimization with secure
compilation . . . . . . . . . . . . . . 142:1--142:30
Florian Lanzinger and
Alexander Weigl and
Mattias Ulbrich and
Werner Dietl Scalability and precision by combining
expressive type systems and deductive
verification . . . . . . . . . . . . . . 143:1--143:29
Angélica Aparecida Moreira and
Guilherme Ottoni and
Fernando Magno Quintão Pereira \pkgVESPA: static profiling for binary
optimization . . . . . . . . . . . . . . 144:1--144:28
Fabian Wolff and
Aurel Bílý and
Christoph Matheja and
Peter Müller and
Alexander J. Summers Modular specification and verification
of closures in Rust . . . . . . . . . . 145:1--145:29
Christian Bräm and
Marco Eilers and
Peter Müller and
Robin Sierra and
Alexander J. Summers Rich specifications for Ethereum smart
contract verification . . . . . . . . . 146:1--146:30
Tian Tan and
Yue Li and
Xiaoxing Ma and
Chang Xu and
Yannis Smaragdakis Making pointer analysis more precise by
unleashing the power of selective
context sensitivity . . . . . . . . . . 147:1--147:27
Guy L. Steele Jr. and
Sebastiano Vigna \pkgLXM: better splittable pseudorandom
number generators (and almost as fast) 148:1--148:31
Karl Cronburg and
Samuel Z. Guyer \pkgPermchecker: a toolchain for
debugging memory managers with typestate 149:1--149:28
Artem Pelenitsyn and
Julia Belyakova and
Benjamin Chung and
Ross Tate and
Jan Vitek Type stability in Julia: avoiding
performance pathologies in JIT
compilation . . . . . . . . . . . . . . 150:1--150:26
Xiaodong Jia and
Ashish Kumar and
Gang Tan A derivative-based parser generator for
visibly pushdown grammars . . . . . . . 151:1--151:24
Jiwon Park and
Dominik Winterer and
Chengyu Zhang and
Zhendong Su Generative type-aware mutation for
testing SMT solvers . . . . . . . . . . 152:1--152:19
Kasra Ferdowsifard and
Shraddha Barke and
Hila Peleg and
Sorin Lerner and
Nadia Polikarpova \pkgLooPy: interactive program synthesis
with control structures . . . . . . . . 153:1--153:29
Michael D. Brown and
Matthew Pruett and
Robert Bigelow and
Girish Mururu and
Santosh Pande Not so fast: understanding and
mitigating negative impacts of compiler
optimizations on code reuse gadget sets 154:1--154:30
Justin Lubin and
Sarah E. Chasins How statically-typed functional
programmers write code . . . . . . . . . 155:1--155:30
Ting Su and
Yichen Yan and
Jue Wang and
Jingling Sun and
Yiheng Xiong and
Geguang Pu and
Ke Wang and
Zhendong Su Fully automated functional fuzzing of
Android apps for detecting non-crashing
logic bugs . . . . . . . . . . . . . . . 156:1--156:31
Nouraldin Jaber and
Christopher Wagner and
Swen Jacobs and
Milind Kulkarni and
Roopsha Samanta \pkgQuickSilver: modeling and
parameterized verification for
distributed agreement-based systems . . 157:1--157:31
Kia Rahmani and
Mohammad Raza and
Sumit Gulwani and
Vu Le and
Daniel Morris and
Arjun Radhakrishna and
Gustavo Soares and
Ashish Tiwari Multi-modal program inference: a
marriage of pre-trained language models
and component-based synthesis . . . . . 158:1--158:29
Mohamad Barbar and
Yulei Sui Compacting points-to sets through object
clustering . . . . . . . . . . . . . . . 159:1--159:27
Satyajit Gokhale and
Alexi Turcotte and
Frank Tip Automatic migration from synchronous to
asynchronous JavaScript APIs . . . . . . 160:1--160:27
Xiang Gao and
Arjun Radhakrishna and
Gustavo Soares and
Ridwan Shariffdeen and
Sumit Gulwani and
Abhik Roychoudhury \pkgAPIfix: output-oriented program
synthesis for combating breaking changes
in libraries . . . . . . . . . . . . . . 161:1--161:27
Arjun Pitchanathan and
Christian Ulmann and
Michel Weber and
Torsten Hoefler and
Tobias Grosser \pkgFPL: fast Presburger arithmetic
through transprecision . . . . . . . . . 162:1--162:26
Yannis Smaragdakis and
Neville Grech and
Sifis Lagouvardos and
Konstantinos Triantafyllou and
Ilias Tsatiris Symbolic value-flow static analysis:
deep, precise, complete modeling of
Ethereum smart contracts . . . . . . . . 163:1--163:30
Truc Lam Bui and
Krishnendu Chatterjee and
Tushar Gautam and
Andreas Pavlogiannis and
Viktor Toman The reads-from equivalence for the TSO
and PSO memory models . . . . . . . . . 164:1--164:30
Alexandru Dura and
Christoph Reichenbach and
Emma Söderberg \pkgJavaDL: automatically
incrementalizing Java bug pattern
detection . . . . . . . . . . . . . . . 165:1--165:31
Nader Al Awar and
Kush Jain and
Christopher J. Rossbach and
Milos Gligoric Programming and execution models for
parallel bounded exhaustive testing . . 166:1--166:28
Ruyi Ji and
Jingtao Xia and
Yingfei Xiong and
Zhenjiang Hu Generalizable synthesis through
unification . . . . . . . . . . . . . . 167:1--167:28
Kevin Batz and
Adrian Gallus and
Benjamin Lucien Kaminski and
Joost-Pieter Katoen and
Tobias Winkler Weighted programming: a programming
paradigm for specifying mathematical
models . . . . . . . . . . . . . . . . . 66:1--66:30
Kostas Ferles and
Benjamin Sepanski and
Rahul Krishnan and
James Bornholt and
Isil Dillig Synthesizing fine-grained
synchronization protocols for implicit
monitors . . . . . . . . . . . . . . . . 67:1--67:26
Chengpeng Wang and
Peisen Yao and
Wensheng Tang and
Qingkai Shi and
Charles Zhang Complexity-guided container replacement
synthesis . . . . . . . . . . . . . . . 68:1--68:31
Jialin Li and
Andrea Lattuada and
Yi Zhou and
Jonathan Cameron and
Jon Howell and
Bryan Parno and
Chris Hawblitzel Linear types for large-scale systems
verification . . . . . . . . . . . . . . 69:1--69:28
Elizabeth Labrada and
Matías Toro and
Éric Tanter and
Dominique Devriese Plausible sealing for gradual
parametricity . . . . . . . . . . . . . 70:1--70:28
Benjamin Mariano and
Yanju Chen and
Yu Feng and
Greg Durrett and
Isil Dillig Automated transpilation of imperative to
functional code using neural-guided
program synthesis . . . . . . . . . . . 71:1--71:27
Peng Yan and
Hanru Jiang and
Nengkun Yu On incorrectness logic for Quantum
programs . . . . . . . . . . . . . . . . 72:1--72:28
Jiawei Liu and
Yuxiang Wei and
Sen Yang and
Yinlin Deng and
Lingming Zhang Coverage-guided tensor compiler fuzzing
with joint IR-pass mutation . . . . . . 73:1--73:26
A\"\ina Linn Georges and
Alix Trieu and
Lars Birkedal Le temps des cérises: efficient temporal
stack safety on capability machines
using directed capabilities . . . . . . 74:1--74:30
Shubham Ugare and
Gagandeep Singh and
Sasa Misailovic Proof transfer for fast certification of
multiple approximate neural networks . . 75:1--75:29
Jonathan Immanuel Brachthäuser and
Philipp Schuster and
Edward Lee and
Aleksander Boruch-Gruszecki Effects, capabilities, and boxes: from
scope-based reasoning to type-based
reasoning and back . . . . . . . . . . . 76:1--76:30
Neville Grech and
Sifis Lagouvardos and
Ilias Tsatiris and
Yannis Smaragdakis Elipmoc: advanced decompilation of
Ethereum smart contracts . . . . . . . . 77:1--77:27
Aravind Machiry and
John Kastner and
Matt McCutchen and
Aaron Eline and
Kyle Headley and
Michael Hicks C to checked C by 3C . . . . . . . . . . 78:1--78:29
Tristan Dyer and
Tim Nelson and
Kathi Fisler and
Shriram Krishnamurthi Applying cognitive principles to
model-finding output: the positive value
of negative information . . . . . . . . 79:1--79:29
Mohsen Lesani and
Li-yao Xia and
Anders Kaseorg and
Christian J. Bell and
Adam Chlipala and
Benjamin C. Pierce and
Steve Zdancewic C4: verified transactional objects . . . 80:1--80:31
Quang Loc Le and
Azalea Raad and
Jules Villard and
Josh Berdine and
Derek Dreyer and
Peter W. O'Hearn Finding real bugs in big programs with
incorrectness logic . . . . . . . . . . 81:1--81:27
Koen Jacobs and
Dominique Devriese and
Amin Timany Purity of an ST monad: full abstraction
by semantically typed back-translation 82:1--82:27
Véronique Benzaken and
Évelyne Contejean and
Mohammed Houssem Hachmaoui and
Chantal Keller and
Louis Mandel and
Avraham Shinnar and
Jérôme Siméon Translating canonical SQL to imperative
code in Coq . . . . . . . . . . . . . . 83:1--83:27
Basile Clément and
Albert Cohen End-to-end translation validation for
the Halide language . . . . . . . . . . 84:1--84:30
Daniel A. A. Pelsmaeker and
Hendrik van Antwerpen and
Casper Bach Poulsen and
Eelco Visser Language-parametric static semantic code
completion . . . . . . . . . . . . . . . 85:1--85:30
Matteo Paltenghi and
Michael Pradel Bugs in Quantum computing platforms: an
empirical study . . . . . . . . . . . . 86:1--86:27
Linpeng Zhang and
Benjamin Lucien Kaminski Quantitative strongest post: a calculus
for reasoning about the flow of
quantitative information . . . . . . . . 87:1--87:29
Bozhen Liu and
Jeff Huang SHARP: fast incremental
context-sensitive pointer analysis for
Java . . . . . . . . . . . . . . . . . . 88:1--88:28
Amir Shaikhha and
Mathieu Huot and
Jaclyn Smith and
Dan Olteanu Functional collection programming with
semi-ring dictionaries . . . . . . . . . 89:1--89:33
Jules Jacobs and
Stephanie Balzer and
Robbert Krebbers Connectivity graphs: a method for
proving deadlock freedom based on
separation logic . . . . . . . . . . . . 1:1--1:33
Chris Heunen and
Robin Kaarsgaard Quantum information effects . . . . . . 2:1--2:27
Jay P. Lim and
Santosh Nagarakatte One polynomial approximation to produce
correctly rounded results of an
elementary function for multiple
representations and rounding modes . . . 3:1--3:28
Bryan Tan and
Benjamin Mariano and
Shuvendu K. Lahiri and
Isil Dillig and
Yu Feng SolType: refinement types for arithmetic
overflow in Solidity . . . . . . . . . . 4:1--4:29
Luca Ciccone and
Luca Padovani Fair termination of binary sessions . . 5:1--5:30
Vikraman Choudhury and
Jacek Karwowski and
Amr Sabry Symmetries in reversible programming:
from symmetric rig groupoids to
reversible programming languages . . . . 6:1--6:32
Roly Perera and
Minh Nguyen and
Tomas Petricek and
Meng Wang Linked visualisations via Galois
dependencies . . . . . . . . . . . . . . 7:1--7:29
Delia Kesner A fine-grained computational
interpretation of Girard's
intuitionistic proof-nets . . . . . . . 8:1--8:28
Yue Niu and
Jonathan Sterling and
Harrison Grodin and
Robert Harper A cost-aware logical framework . . . . . 9:1--9:31
Paul Krogmeier and
P. Madhusudan Learning formulas in finite variable
logics . . . . . . . . . . . . . . . . . 10:1--10:28
Jean-Marie Madiot and
François Pottier A separation logic for heap space under
garbage collection . . . . . . . . . . . 11:1--11:28
Adam Husted Kjelstròm and
Andreas Pavlogiannis The decidability and complexity of
interleaved bidirected Dyck reachability 12:1--12:26
Giuseppe Castagna and
Mickaël Laurent and
Kim Nguy\~ên and
Matthew Lutze On type-cases, union elimination, and
occurrence typing . . . . . . . . . . . 13:1--13:31
Zi Wang and
Aws Albarghouthi and
Gautam Prakriya and
Somesh Jha Interval universal approximation for
neural networks . . . . . . . . . . . . 14:1--14:29
Yotam M. Y. Feldman and
Mooly Sagiv and
Sharon Shoham and
James R. Wilcox Property-directed reachability as
abstract interpretation in the monotone
theory . . . . . . . . . . . . . . . . . 15:1--15:31
Yizhou Zhang and
Nada Amin Reasoning about ``reasoning about
reasoning'': semantics and contextual
equivalence for probabilistic programs
with nested queries and recursion . . . 16:1--16:28
Pascal Baumann and
Rupak Majumdar and
Ramanathan S. Thinniyam and
Georg Zetzsche Context-bounded verification of thread
pools . . . . . . . . . . . . . . . . . 17:1--17:28
Davide Sangiorgi From enhanced coinduction towards
enhanced induction . . . . . . . . . . . 18:1--18:29
Ugo Dal Lago and
Francesco Gavazzo Effectful program distancing . . . . . . 19:1--19:30
Rodolphe Lepigre and
Michael Sammler and
Kayvan Memarian and
Robbert Krebbers and
Derek Dreyer and
Peter Sewell VIP: verifying real-world C idioms with
integer-pointer casts . . . . . . . . . 20:1--20:32
Anders Miltner and
Adrian Trejo Nuñez and
Ana Brendel and
Swarat Chaudhuri and
Isil Dillig Bottom-up synthesis of recursive
functional programs using angelic
execution . . . . . . . . . . . . . . . 21:1--21:29
Azalea Raad and
Luc Maranget and
Viktor Vafeiadis Extending Intel-x86 consistency and
persistency: formalising the semantics
of Intel-x86 memory types and
non-temporal stores . . . . . . . . . . 22:1--22:31
Andrew K. Hirsch and
Deepak Garg Pirouette: higher-order typed functional
choreographies . . . . . . . . . . . . . 23:1--23:27
Mirai Ikebuchi and
Andres Erbsen and
Adam Chlipala Certifying derivation of state machines
from coroutines . . . . . . . . . . . . 24:1--24:31
Yuting Wang and
Ling Zhang and
Zhong Shao and
Jérémie Koenig Verified compilation of C programs with
a nominal memory model . . . . . . . . . 25:1--25:31
Xiaodong Jia and
Andre Kornell and
Bert Lindenhovius and
Michael Mislove and
Vladimir Zamdzhiev Semantics for variational Quantum
programming . . . . . . . . . . . . . . 26:1--26:31
Matthew Kolosick and
Shravan Narayan and
Evan Johnson and
Conrad Watt and
Michael LeMay and
Deepak Garg and
Ranjit Jhala and
Deian Stefan Isolation without taxation:
near-zero-cost transitions for
WebAssembly and SFI . . . . . . . . . . 27:1--27:30
Lennard Gäher and
Michael Sammler and
Simon Spies and
Ralf Jung and
Hoang-Hai Dang and
Robbert Krebbers and
Jeehoon Kang and
Derek Dreyer Simuliris: a separation logic framework
for verifying concurrent program
optimizations . . . . . . . . . . . . . 28:1--28:31
Cheng Zhang and
Arthur Azevedo de Amorim and
Marco Gaboardi On incorrectness logic and Kleene
algebra with top and tests . . . . . . . 29:1--29:30
Charles Yuan and
Christopher McNally and
Michael Carbin Twist: sound reasoning for purity and
entanglement in Quantum programs . . . . 30:1--30:32
Ugo Dal Lago and
Francesco Gavazzo A relational theory of effects and
coeffects . . . . . . . . . . . . . . . 31:1--31:28
Lo\"\ic Pujet and
Nicolas Tabareau Observational equality: now for good . . 32:1--32:27
Joakim Öhman and
Aleksandar Nanevski Visibility reasoning for concurrent
snapshot algorithms . . . . . . . . . . 33:1--33:30
Azalea Raad and
Josh Berdine and
Derek Dreyer and
Peter W. O'Hearn Concurrent incorrectness separation
logic . . . . . . . . . . . . . . . . . 34:1--34:29
Yihong Zhang and
Yisu Remy Wang and
Max Willsey and
Zachary Tatlock Relational e-matching . . . . . . . . . 35:1--35:22
Xuan-Bach Le and
Shang-Wei Lin and
Jun Sun and
David Sanan A Quantum interpretation of separating
conjunction for local reasoning of
Quantum programs based on separation
logic . . . . . . . . . . . . . . . . . 36:1--36:27
Olivier Blanvillain and
Jonathan Immanuel Brachthäuser and
Maxime Kjaer and
Martin Odersky Type-level programming with match types 37:1--37:24
Devon Loehr and
David Walker Safe, modular packet pipeline
programming . . . . . . . . . . . . . . 38:1--38:28
Junyoung Jang and
Samuel Gélineau and
Stefan Monnier and
Brigitte Pientka Moebius: metaprogramming using
contextual types: the stage where system
f can pattern match on itself . . . . . 39:1--39:27
Matthias Eichholz and
Eric Hayden Campbell and
Matthias Krebs and
Nate Foster and
Mira Mezini Dependently-typed data plane programming 40:1--40:28
Dmitry Chistikov and
Rupak Majumdar and
Philipp Schepper Subcubic certificates for CFL
reachability . . . . . . . . . . . . . . 41:1--41:29
Arthur Oliveira Vale and
Paul-André Melli\`es and
Zhong Shao and
Jérémie Koenig and
Léo Stefanesco Layered and object-based game semantics 42:1--42:32
Mark Niklas Müller and
Gleb Makarchuk and
Gagandeep Singh and
Markus Püschel and
Martin Vechev PRIMA: general and precise neural
network certification via scalable
convex hull approximations . . . . . . . 43:1--43:33
Ohad Kammar and
Shin-ya Katsumata and
Philip Saville Fully abstract models for effectful $
\lambda $-calculi via category-theoretic
logical relations . . . . . . . . . . . 44:1--44:28
Taolue Chen and
Alejandro Flores-Lamas and
Matthew Hague and
Zhilei Han and
Denghang Hu and
Shuanglong Kan and
Anthony W. Lin and
Philipp Rümmer and
Zhilin Wu Solving string constraints with
Regex-dependent functions through
transducers with priorities and
variables . . . . . . . . . . . . . . . 45:1--45:31
Stefan K. Muller Static prediction of parallel
computation graphs . . . . . . . . . . . 46:1--46:31
Sorawee Porncharoenwase and
Luke Nelson and
Xi Wang and
Emina Torlak A formal foundation for symbolic
evaluation with merging . . . . . . . . 47:1--47:28
Faustyna Krawiec and
Simon Peyton Jones and
Neel Krishnaswami and
Tom Ellis and
Richard A. Eisenberg and
Andrew Fitzgibbon Provably correct, asymptotically
efficient, higher-order reverse-mode
automatic differentiation . . . . . . . 48:1--48:30
Michalis Kokologiannakis and
Iason Marmanis and
Vladimir Gladstein and
Viktor Vafeiadis Truly stateless, optimal dynamic partial
order reduction . . . . . . . . . . . . 49:1--49:28
Oded Padon and
James R. Wilcox and
Jason R. Koenig and
Kenneth L. McMillan and
Alex Aiken Induction duality: primal-dual search
for invariants . . . . . . . . . . . . . 50:1--50:29
Qianchuan Ye and
Benjamin Delaware Oblivious algebraic data types . . . . . 51:1--51:29
Wenlei He and
Julián Mestre and
Sergey Pupyrev and
Lei Wang and
Hongtao Yu Profile inference revisited . . . . . . 52:1--52:24
Marcelo Fiore and
Dmitrij Szamozvancev Formal metatheory of second-order
abstract syntax . . . . . . . . . . . . 53:1--53:29
Alan Jeffrey and
James Riely and
Mark Batty and
Simon Cooksey and
Ilya Kaysin and
Anton Podkopaev The leaky semicolon: compositional
semantic dependencies for relaxed-memory
concurrency . . . . . . . . . . . . . . 54:1--54:30
Amanda Liu and
Gilbert Louis Bernstein and
Adam Chlipala and
Jonathan Ragan-Kelley Verified tensor-program optimization via
high-level scheduling rewrites . . . . . 55:1--55:28
Jacob Laurel and
Rem Yang and
Gagandeep Singh and
Sasa Misailovic A dual number abstraction for static
analysis of Clarke Jacobians . . . . . . 56:1--56:30
Jialu Bao and
Marco Gaboardi and
Justin Hsu and
Joseph Tassarotti A separation logic for negative
dependence . . . . . . . . . . . . . . . 57:1--57:29
Minseok Jeon and
Hakjoo Oh Return of CFA: call-site sensitivity can
be superior to object sensitivity even
for object-oriented programs . . . . . . 58:1--58:29
Marco Campion and
Mila Dalla Preda and
Roberto Giacobazzi Partial (In)Completeness in abstract
interpretation: limiting the imprecision
in program analysis . . . . . . . . . . 59:1--59:31
Hari Govind V. K. and
Sharon Shoham and
Arie Gurfinkel Solving constrained Horn clauses modulo
algebraic data types and recursive
functions . . . . . . . . . . . . . . . 60:1--60:29
Ningning Xie and
Matthew Pickering and
Andres Löh and
Nicolas Wu and
Jeremy Yallop and
Meng Wang Staging with class: a specification for
typed template Haskell . . . . . . . . . 61:1--61:30
Yuanbo Li and
Kris Satya and
Qirun Zhang Efficient algorithms for dynamic
bidirected Dyck-reachability . . . . . . 62:1--62:29
Takeshi Tsukada and
Hiroshi Unno Software model-checking as cyclic-proof
search . . . . . . . . . . . . . . . . . 63:1--63:29
Kuen-Bang Hou (Favonia) and
Zhuyang Wang Logarithm and program testing . . . . . 64:1--64:26
Toghrul Karimov and
Engel Lefaucheux and
Joël Ouaknine and
David Purser and
Anton Varonka and
Markus A. Whiteland and
James Worrell What's decidable about linear loops? . . 65:1--65:25
Norman Ramsey Beyond Relooper: recursive translation
of unstructured control flow to
structured control flow (functional
pearl) . . . . . . . . . . . . . . . . . 90:1--90:??
James Koppel and
Zheng Guo and
Edsko de Vries and
Armando Solar-Lezama and
Nadia Polikarpova Searching entangled program spaces . . . 91:1--91:??
Marek Materzok Generating circuits with generators . . 92:1--92:??
Patrick Bahr and
Graham Hutton Monadic compiler calculation (functional
pearl) . . . . . . . . . . . . . . . . . 93:1--93:??
Ma\lgorzata Biernacka and
Witold Charatonik and
Tomasz Drab A simple and efficient implementation of
strong call by need by an abstract
machine . . . . . . . . . . . . . . . . 94:1--94:??
Arnaud Spiwack and
Csongor Kiss and
Jean-Philippe Bernardy and
Nicolas Wu and
Richard A. Eisenberg Linearly qualified types: generic
inference for capabilities and
uniqueness . . . . . . . . . . . . . . . 95:1--95:??
Joseph Eremondi and
Ronald Garcia and
Éric Tanter Propositional equality for gradual
dependently typed programming . . . . . 96:1--96:??
Steven Keuchel and
Sander Huyghebaert and
Georgy Lukyanov and
Dominique Devriese Verified symbolic execution with Kripke
specification monads (and no
meta-programming) . . . . . . . . . . . 97:1--97:??
Hsiang-Shang Ko and
Liang-Ting Chen and
Tzu-Chi Lin Datatype-generic programming meets
elaborator reflection . . . . . . . . . 98:1--98:??
Irene Yoon and
Yannick Zakowski and
Steve Zdancewic Formal reasoning about layered monadic
interpreters . . . . . . . . . . . . . . 99:1--99:??
Simon Spies and
Lennard Gäher and
Joseph Tassarotti and
Ralf Jung and
Robbert Krebbers and
Lars Birkedal and
Derek Dreyer Later credits: resourceful reasoning for
the later modality . . . . . . . . . . . 100:1--100:??
Yao Li and
Stephanie Weirich Program adverbs and Tlön embeddings . . . 101:1--101:??
Elijah Rivera and
Shriram Krishnamurthi Structural versus pipeline composition
of higher-order functions (experience
report) . . . . . . . . . . . . . . . . 102:1--102:??
Anton Lorenzen and
Daan Leijen Reference counting with frame limited
reuse . . . . . . . . . . . . . . . . . 103:1--103:??
Minh Nguyen and
Roly Perera and
Meng Wang and
Nicolas Wu Modular probabilistic models via
algebraic effects . . . . . . . . . . . 104:1--104:??
Cas van der Rest and
Wouter Swierstra A completely unique account of
enumeration . . . . . . . . . . . . . . 105:1--105:??
Klaus Ostermann and
David Binder and
Ingo Skupin and
Tim Süberkrüb and
Paul Downen Introduction and elimination, left and
right . . . . . . . . . . . . . . . . . 106:1--106:??
Jules Jacobs and
Stephanie Balzer and
Robbert Krebbers Multiparty GV: functional multiparty
session types with certified deadlock
freedom . . . . . . . . . . . . . . . . 107:1--107:??
Patrick Thomson and
Rob Rix and
Nicolas Wu and
Tom Schrijvers Fusing industry and academia at GitHub
(experience report) . . . . . . . . . . 108:1--108:??
Sebastian Ullrich and
Leonardo de Moura `do' unchained: embracing local
imperativity in a purely functional
language (functional pearl) . . . . . . 109:1--109:??
András Kovács Staged compilation with two-level type
theory . . . . . . . . . . . . . . . . . 110:1--110:??
Frank Emrich and
Jan Stolarek and
James Cheney and
Sam Lindley Constraint-based type inference for
FreezeML . . . . . . . . . . . . . . . . 111:1--111:??
Elizaveta Vasilenko and
Niki Vazou and
Gilles Barthe Safe couplings: coupled refinement types 112:1--112:??
Lucas Escot and
Jesper Cockx Practical generic programming over a
universe of native datatypes . . . . . . 113:1--113:??
Benjamin Quiring and
John Reppy and
Olin Shivers Analyzing binding extent in 3CPS . . . . 114:1--114:??
Sam Westrick and
Jatin Arora and
Umut A. Acar Entanglement detection with near-zero
cost . . . . . . . . . . . . . . . . . . 115:1--115:??
Son Ho and
Jonathan Protzenko Aeneas: Rust verification by functional
translation . . . . . . . . . . . . . . 116:1--116:??
James Koppel and
Jackson Kearl and
Armando Solar-Lezama Automatically deriving control-flow
graph generators from operational
semantics . . . . . . . . . . . . . . . 117:1--117:??
Nachiappan Valliappan and
Fabian Ruch and
Carlos Tomé Cortiñas Normalization for fitch-style modal
calculi . . . . . . . . . . . . . . . . 118:1--118:??
Beniamino Accattoli and
Ugo Dal Lago and
Gabriele Vanoni Multi types and reasonable space . . . . 119:1--119:??
Gilles Barthe and
Raphaëlle Crubillé and
Ugo Dal Lago and
Francesco Gavazzo On Feller continuity and full
abstraction . . . . . . . . . . . . . . 120:1--120:??
Beniamino Accattoli and
Giulio Guerrieri The theory of call-by-value solvability 121:1--121:??
Tram Hoang and
Anton Trunov and
Leonidas Lampropoulos and
Ilya Sergey Random testing of a higher-order
blockchain language (experience report) 122:1--122:??
Shin-ya Katsumata and
Dylan McDermott and
Tarmo Uustalu and
Nicolas Wu Flexible presentations of graded monads 123:1--123:??
Kenji Maillard and
Meven Lennon-Bertrand and
Nicolas Tabareau and
Éric Tanter A reasonably gradual type theory . . . . 124:1--124:??
Fabian Ritter and
Sebastian Hack AnICA: analyzing inconsistencies in
microarchitectural code analyzers . . . 125:1--125:??
Ningning Xie and
Youyou Cong and
Kazuki Ikemori and
Daan Leijen First-class names for effect handlers 126:1--126:??
Mengqi Liu and
Zhong Shao and
Hao Chen and
Man-Ki Yoon and
Jung-Eun Kim Compositional virtual timelines:
verifying dynamic-priority partitions
with algorithmic temporal isolation . . 127:1--127:??
Harrison Goldstein and
Benjamin C. Pierce Parsing randomness . . . . . . . . . . . 128:1--128:??
Thomas Haas and
Roland Meyer and
Hernán Ponce de León CAAT: consistency as a theory . . . . . 129:1--129:??
Emma Ahrens and
Marius Bozga and
Radu Iosif and
Joost-Pieter Katoen Reasoning about distributed
reconfigurable systems . . . . . . . . . 130:1--130:??
Yaozhu Sun and
Utkarsh Dhandhania and
Bruno C. d. S. Oliveira Compositional embeddings of
domain-specific languages . . . . . . . 131:1--131:??
Hongming Liu and
Hongfei Fu and
Zhiyong Yu and
Jiaxin Song and
Guoqiang Li Scalable linear invariant generation
with Farkas' lemma . . . . . . . . . . . 132:1--132:??
Nico Ritschel and
Felipe Fronchetti and
Reid Holmes and
Ronald Garcia and
David C. Shepherd Can guided decomposition help end-users
write larger block-based programs? A
mobile robot experiment . . . . . . . . 133:1--133:??
Charles Yuan and
Michael Carbin Tower: data structures in Quantum
superposition . . . . . . . . . . . . . 134:1--134:??
Emanuele D'Osualdo and
Azadeh Farzan and
Derek Dreyer Proving hypersafety compositionally . . 135:1--135:??
Si Liu and
Jose Meseguer and
Peter Csaba Ölveczky and
Min Zhang and
David Basin Bridging the semantic gap between
qualitative and quantitative models of
distributed systems . . . . . . . . . . 136:1--136:??
Gal Sela and
Erez Petrank Concurrent size . . . . . . . . . . . . 137:1--137:??
Kevin Bierhoff Wildcards need witness protection . . . 138:1--138:??
Yuhao Zhang and
Yasharth Bajpai and
Priyanshu Gupta and
Ameya Ketkar and
Miltiadis Allamanis and
Titus Barik and
Sumit Gulwani and
Arjun Radhakrishna and
Mohammad Raza and
Gustavo Soares and
Ashish Tiwari Overwatch: learning patterns in code
edit sequences . . . . . . . . . . . . . 139:1--139:??
Aron Zwaan and
Hendrik van Antwerpen and
Eelco Visser Incremental type-checking for free:
using scope graphs to derive incremental
type-checkers . . . . . . . . . . . . . 140:1--140:??
Lionel Parreaux and
Chun Yin Chau MLstruct: principal type inference in a
Boolean algebra of structural types . . 141:1--141:??
Joshua Hoeflich and
Robert Bruce Findler and
Manuel Serrano Highly illogical, Kirk: spotting type
mismatches in the large despite broken
contracts, unsound types, and too many
linters . . . . . . . . . . . . . . . . 142:1--142:??
Aishwarya Sivaraman and
Alex Sanchez-Stern and
Bretton Chen and
Sorin Lerner and
Todd Millstein Data-driven lemma synthesis for
interactive proofs . . . . . . . . . . . 143:1--143:??
Qiaochu Chen and
Shankara Pailoor and
Celeste Barnaby and
Abby Criswell and
Chenglong Wang and
Greg Durrett and
I\csil Dillig Type-directed synthesis of
visualizations from natural language
queries . . . . . . . . . . . . . . . . 144:1--144:??
Yanju Chen and
Yuepeng Wang and
Maruth Goyal and
James Dong and
Yu Feng and
I\csil Dillig Synthesis-powered optimization of smart
contracts via data type refactoring . . 145:1--145:??
Liyi Li and
Finn Voichick and
Kesha Hietala and
Yuxiang Peng and
Xiaodi Wu and
Michael Hicks Verified compilation of quantum oracles 146:1--146:??
Ashish Mishra and
Suresh Jagannathan Specification-guided component-based
synthesis from effectful libraries . . . 147:1--147:??
Ben L. Titzer A fast in-place interpreter for
WebAssembly . . . . . . . . . . . . . . 148:1--148:??
Zihan Zhao and
Sidi Mohamed Beillahi and
Ryan Song and
Yuxi Cai and
Andreas Veneris and
Fan Long SigVM: enabling event-driven execution
for truly decentralized smart contracts 149:1--149:??
Chiké Abuah and
David Darais and
Joseph P. Near Solo: a lightweight static analysis for
differential privacy . . . . . . . . . . 150:1--150:??
Clément Blaudeau and
Fengyun Liu A conceptual framework for safe object
initialization: a principled and
mechanized soundness proof of the
Celsius model . . . . . . . . . . . . . 151:1--151:??
Evgenii Moiseenko and
Michalis Kokologiannakis and
Viktor Vafeiadis Model checking for a multi-execution
memory model . . . . . . . . . . . . . . 152:1--152:??
Khushboo Chitre and
Piyus Kedia and
Rahul Purandare The road not taken: exploring alias
analysis based optimizations missed by
the compiler . . . . . . . . . . . . . . 153:1--153:??
Julian Mackay and
Susan Eisenbach and
James Noble and
Sophia Drossopoulou Necessity specifications for robustness 154:1--154:??
Dan Frumin and
Emanuele D'Osualdo and
Bas van den Heuvel and
Jorge A. Pérez A bunch of sessions: a
propositions-as-sessions interpretation
of bunched implications in channel-based
concurrency . . . . . . . . . . . . . . 155:1--155:??
Riccardo Bianchini and
Francesco Dagnino and
Paola Giannini and
Elena Zucca and
Marco Servetto Coeffects for sharing and mutation . . . 156:1--156:??
Philip Dexter and
Yu David Liu and
Kenneth Chiu The essence of online data processing 157:1--157:??
Zhihang Sun and
Hongyu Fan and
Fei He Consistency-preserving propagation for
SMT solving of concurrent program
verification . . . . . . . . . . . . . . 158:1--158:??
Daming Zou and
Yuchen Gu and
Yuanfeng Shi and
MingZhe Wang and
Yingfei Xiong and
Zhendong Su Oracle-free repair synthesis for
floating-point programs . . . . . . . . 159:1--159:??
Marisa Kirisame and
Pranav Shenoy and
Pavel Panchekha Optimal heap limits for reducing browser
memory use . . . . . . . . . . . . . . . 160:1--160:??
Jacob Laurel and
Rem Yang and
Shubham Ugare and
Robert Nagel and
Gagandeep Singh and
Sasa Misailovic A general construction for abstract
interpretation of higher-order automatic
differentiation . . . . . . . . . . . . 161:1--161:??
Haoze Wu and
Clark Barrett and
Mahmood Sharif and
Nina Narodytska and
Gagandeep Singh Scalable verification of GNN-based job
schedulers . . . . . . . . . . . . . . . 162:1--162:??
Thibault Dardinier and
Peter Müller and
Alexander J. Summers Fractional resources in unbounded
separation logic . . . . . . . . . . . . 163:1--163:??
Rohan Bavishi and
Harshit Joshi and
José Cambronero and
Anna Fariha and
Sumit Gulwani and
Vu Le and
Ivan Radi\vcek and
Ashish Tiwari Neurosymbolic repair for low-code
formula languages . . . . . . . . . . . 164:1--164:??
Stefanos Chaliasos and
Arthur Gervais and
Benjamin Livshits A study of inline assembly in Solidity
smart contracts . . . . . . . . . . . . 165:1--165:??
Charles Jin and
Phitchaya Mangpo Phothilimthana and
Sudip Roy Neural architecture search using
property guided synthesis . . . . . . . 166:1--166:??
Georgios Sakkas and
Madeline Endres and
Philip J. Guo and
Westley Weimer and
Ranjit Jhala Seq2Parse: neurosymbolic parse error
repair . . . . . . . . . . . . . . . . . 167:1--167:??
Stephen Ellis and
Shuofei Zhu and
Nobuko Yoshida and
Linhai Song Generic go to go: dictionary-passing,
monomorphisation, and hybrid . . . . . . 168:1--168:??
Sujit Kumar Muduli and
Subhajit Roy Satisfiability modulo fuzzing: a
synergistic combination of SMT solving
and fuzzing . . . . . . . . . . . . . . 169:1--169:??
Kirshanthan Sundararajah and
Charitha Saumya and
Milind Kulkarni UniRec: a unimodular-like framework for
nested recursions and loops . . . . . . 170:1--170:??
Pankaj Kumar Kalita and
Sujit Kumar Muduli and
Loris D'Antoni and
Thomas Reps and
Subhajit Roy Synthesizing abstract transformers . . . 171:1--171:??
Pritam Choudhury Monadic and comonadic aspects of
dependency analysis . . . . . . . . . . 172:1--172:??
Shadaj Laddad and
Conor Power and
Mae Milano and
Alvin Cheung and
Joseph M. Hellerstein Katara: synthesizing CRDTs with verified
lifting . . . . . . . . . . . . . . . . 173:1--173:??
Roland Meyer and
Thomas Wies and
Sebastian Wolff A concurrent program logic with a future
and history . . . . . . . . . . . . . . 174:1--174:??
Stephen Chou and
Saman Amarasinghe Compilation of dynamic sparse tensor
algebra . . . . . . . . . . . . . . . . 175:1--175:??
Qingkai Shi and
Yongchao Wang and
Peisen Yao and
Charles Zhang Indexing the extended Dyck-CFL
reachability for context-sensitive
program analysis . . . . . . . . . . . . 176:1--176:??
John C. Kolesar and
Ruzica Piskac and
William T. Hallahan Checking equivalence in a non-strict
language . . . . . . . . . . . . . . . . 177:1--177:??
Marcel Moosbrugger and
Miroslav Stankovi\vc and
Ezio Bartocci and
Laura Kovács This is the moment for probabilistic
loops . . . . . . . . . . . . . . . . . 178:1--178:??
Aleksander Boruch-Gruszecki and
Rados\law Wa\'sko and
Yichen Xu and
Lionel Parreaux A case for DOT: theoretical foundations
for objects with pattern matching and
GADT-style reasoning . . . . . . . . . . 179:1--179:??
Yuxiang Lei and
Yulei Sui and
Shuo Ding and
Qirun Zhang Taming transitive redundancy for
context-free language reachability . . . 180:1--180:??
Zachary Susag and
Sumit Lahiri and
Justin Hsu and
Subhajit Roy Symbolic execution for randomized
programs . . . . . . . . . . . . . . . . 181:1--181:??
Fengmin Zhu and
Michael Sammler and
Rodolphe Lepigre and
Derek Dreyer and
Deepak Garg BFF: foundational and automated
verification of bitfield-manipulating
programs . . . . . . . . . . . . . . . . 182:1--182:??
Dan Ghica and
Sam Lindley and
Marcos Maroñas Bravo and
Maciej Piróg High-level effect handlers in C++ . . . 183:1--183:??
Eric Atkinson and
Charles Yuan and
Guillaume Baudart and
Louis Mandel and
Michael Carbin Semi-symbolic inference for efficient
streaming probabilistic programming . . 184:1--184:??
Paul Krogmeier and
Zhengyao Lin and
Adithya Murali and
P. Madhusudan Synthesizing axiomatizations using logic
learning . . . . . . . . . . . . . . . . 185:1--185:??
Adam Chen and
Parisa Fathololumi and
Eric Koskinen and
Jared Pincus Veracity: declarative multicore
programming with commutativity . . . . . 186:1--186:??
Pranav Garg and
Srinivasan H. Sengamedu Synthesizing code quality rules from
examples . . . . . . . . . . . . . . . . 187:1--187:??
Abel Nieto and
Léon Gondelman and
Alban Reynaud and
Amin Timany and
Lars Birkedal Modular verification of op-based CRDTs
in separation logic . . . . . . . . . . 188:1--188:??
Sadegh Dalvandi and
Brijesh Dongol Implementing and verifying
release--acquire transactional memory in
C11 . . . . . . . . . . . . . . . . . . 189:1--189:??
Sangeeta Chowdhary and
Santosh Nagarakatte Fast shadow execution for debugging
numerical errors using error free
transformations . . . . . . . . . . . . 190:1--190:??
Adithya Murali and
Lucas Peña and
Eion Blanchard and
Christof Löding and
P. Madhusudan Model-guided synthesis of inductive
lemmas for FOL with least fixpoints . . 191:1--191:??
Cas van der Rest and
Casper Bach Poulsen and
Arjen Rouvoet and
Eelco Visser and
Peter Mosses Intrinsically-typed definitional
interpreters \`a la carte . . . . . . . 192:1--192:??
Christopher Pulte and
Dhruv C. Makwana and
Thomas Sewell and
Kayvan Memarian and
Peter Sewell and
Neel Krishnaswami CN: Verifying Systems C Code with
Separation-Logic Refinement Types . . . 1:1--1:??
Alejandro Aguirre and
Lars Birkedal Step-Indexed Logical Relations for
Countable Nondeterminism and
Probabilistic Choice . . . . . . . . . . 2:1--2:??
Pedro Abreu and
Benjamin Delaware and
Alex Hubers and
Christa Jenkins and
J. Garrett Morris and
Aaron Stump A Type-Based Approach to
Divide-and-Conquer Recursion in Coq . . 3:1--3:??
Yanjun Wang and
Zixuan Li and
Chuan Jiang and
Xiaokang Qiu and
Sanjay Rao Comparative Synthesis: Learning
Near-Optimal Network Designs by Query 4:1--4:??
Alexander K. Lew and
Mathieu Huot and
Sam Staton and
Vikash K. Mansinghka ADEV: Sound Automatic Differentiation of
Expected Values of Probabilistic
Programs . . . . . . . . . . . . . . . . 5:1--5:??
Naoki Kobayashi and
Kento Tanahashi and
Ryosuke Sato and
Takeshi Tsukada HFL(Z) Validity Checking for Automated
Program Verification . . . . . . . . . . 6:1--6:??
Aaron Bembenek and
Michael Greenberg and
Stephen Chong From SMT to ASP: Solver-Based Approaches
to Solving Datalog
Synthesis-as-Rule-Selection Problems . . 7:1--7:??
Axel Kerinec and
Giulio Manzonetto and
Federico Olimpieri Why Are Proofs Relevant in
Proof-Relevant Models? . . . . . . . . . 8:1--8:??
Aur\`ele Barri\`ere and
Sandrine Blazy and
David Pichardie Formally Verified Native Code Generation
in an Effectful JIT: Turning the
CompCert Backend into a Formally
Verified JIT Compiler . . . . . . . . . 9:1--9:??
Joel D. Day and
Vijay Ganesh and
Nathan Grewal and
Florin Manea On the Expressive Power of String
Constraints . . . . . . . . . . . . . . 10:1--10:??
Peng Fu and
Kohei Kishida and
Neil J. Ross and
Peter Selinger Proto-Quipper with Dynamic Lifting . . . 11:1--11:??
Wonyeol Lee and
Xavier Rival and
Hongseok Yang Smoothness Analysis for Probabilistic
Programs with Application to Optimised
Variational Inference . . . . . . . . . 12:1--12:??
Konstantinos Kallas and
Haoran Zhang and
Rajeev Alur and
Sebastian Angel and
Vincent Liu Executing Microservice Applications on
Serverless, Correctly . . . . . . . . . 13:1--13:??
David Cao and
Rose Kunkel and
Chandrakana Nandi and
Max Willsey and
Zachary Tatlock and
Nadia Polikarpova \pkgbabble: Learning Better Abstractions
with E-Graphs and Anti-unification . . . 14:1--14:??
Alexandra E. Michael and
Anitha Gollamudi and
Jay Bosamiya and
Evan Johnson and
Aidan Denlinger and
Craig Disselkoen and
Conrad Watt and
Bryan Parno and
Marco Patrignani and
Marco Vassena and
Deian Stefan MSWasm: Soundly Enforcing Memory-Safe
Execution of Unsafe Code . . . . . . . . 15:1--15:??
Sirui Lu and
Rastislav Bodík \pkgGrisette: Symbolic Compilation as a
Functional Programming Library . . . . . 16:1--16:??
Andrew M. Pitts Locally Nameless Sets . . . . . . . . . 17:1--17:??
Nick Rioux and
Xuejing Huang and
Bruno C. d. S. Oliveira and
Steve Zdancewic A Bowtie for a Beast: Overloading, Eta
Expansion, and Extensible Data Types in
F$ \bowtie $ . . . . . . . . . . . . . . 18:1--18:??
Michalis Kokologiannakis and
Ori Lahav and
Viktor Vafeiadis \pkgKater: Automating Weak Memory Model
Metatheory and Consistency Checking . . 19:1--19:??
Timos Antonopoulos and
Eric Koskinen and
Ton Chanh Le and
Ramana Nagasamudram and
David A. Naumann and
Minh Ngo An Algebra of Alignment for Relational
Verification . . . . . . . . . . . . . . 20:1--20:??
Yu Gu and
Takeshi Tsukada and
Hiroshi Unno Optimal CHC Solving via Termination
Proofs . . . . . . . . . . . . . . . . . 21:1--21:??
Sergey Goncharov and
Stefan Milius and
Lutz Schröder and
Stelios Tsampas and
Henning Urbat Towards a Higher-Order Mathematical
Operational Semantics . . . . . . . . . 22:1--22:??
Jinwoo Kim and
Loris D\textquotesingleAntoni and
Thomas Reps Unrealizability Logic . . . . . . . . . 23:1--23:??
Simon Castellan and
Pierre Clairambault The Geometry of Causality: Multi-token
Geometry of Interaction and Its Causal
Unfolding . . . . . . . . . . . . . . . 24:1--24:??
Alexandre Moine and
Arthur Charguéraud and
François Pottier A High-Level Separation Logic for Heap
Space under Garbage Collection . . . . . 25:1--25:??
Emanuele D\textquotesingleOsualdo and
Azalea Raad and
Viktor Vafeiadis The Path to Durable Linearizability . . 26:1--26:??
Michael Sammler and
Simon Spies and
Youngju Song and
Emanuele D\textquotesingleOsualdo and
Robbert Krebbers and
Deepak Garg and
Derek Dreyer DimSum: a Decentralized Approach to
Multi-language Semantics and
Verification . . . . . . . . . . . . . . 27:1--27:??
Emmanuel Hainry and
Romain Péchoux A General Noninterference Policy for
Polynomial Time . . . . . . . . . . . . 28:1--28:??
Li Zhou and
Gilles Barthe and
Pierre-Yves Strub and
Junyi Liu and
Mingsheng Ying CoqQ: Foundational Verification of
Quantum Programs . . . . . . . . . . . . 29:1--29:??
Joshua Gancher and
Kristina Sojakova and
Xiong Fan and
Elaine Shi and
Greg Morrisett A Core Calculus for Equational Proofs of
Cryptographic Protocols . . . . . . . . 30:1--30:??
Han Xu and
Xuejing Huang and
Bruno C. d. S. Oliveira Making a Type Difference: Subtraction on
Intersection Types as Generalized Record
Operations . . . . . . . . . . . . . . . 31:1--31:??
Finn Voichick and
Liyi Li and
Robert Rand and
Michael Hicks \pkgQunity: a Unified Language for
Quantum and Classical Computing . . . . 32:1--32:??
José Cambronero and
Sumit Gulwani and
Vu Le and
Daniel Perelman and
Arjun Radhakrishna and
Clint Simon and
Ashish Tiwari \pkgFlashFill++: Scaling Programming by
Example by Cutting to the Chase . . . . 33:1--33:??
Shuo Ding and
Qirun Zhang Witnessability of Undecidable Problems 34:1--34:??
Yuanbo Li and
Qirun Zhang and
Thomas Reps Single-Source-Single-Target
Interleaved-Dyck Reachability via
Integer Linear Programming . . . . . . . 35:1--35:??
Jules Jacobs and
Stephanie Balzer Higher-Order Leak and Deadlock Free
Locks . . . . . . . . . . . . . . . . . 36:1--36:??
Rajeev Alur and
Caleb Stanford and
Christopher Watson A Robust Theory of Series Parallel
Graphs . . . . . . . . . . . . . . . . . 37:1--37:??
Arthur Oliveira Vale and
Zhong Shao and
Yixuan Chen A Compositional Theory of
Linearizability . . . . . . . . . . . . 38:1--38:??
Youngju Song and
Minki Cho and
Dongjae Lee and
Chung-Kil Hur and
Michael Sammler and
Derek Dreyer Conditional Contextual Refinement . . . 39:1--39:??
Daan Leijen and
Anton Lorenzen Tail Recursion Modulo Context: an
Equational Approach . . . . . . . . . . 40:1--40:??
Matthew Bowers and
Theo X. Olausson and
Lionel Wong and
Gabriel Grand and
Joshua B. Tenenbaum and
Kevin Ellis and
Armando Solar-Lezama Top-Down Synthesis for Library Learning 41:1--41:??
Andrei Popescu and
Dmitriy Traytel Admissible Types-to-PERs Relativization
in Higher-Order Logic . . . . . . . . . 42:1--42:??
Alexey Radul and
Adam Paszke and
Roy Frostig and
Matthew J. Johnson and
Dougal Maclaurin You Only Linearize Once: Tangents
Transpose to Gradients . . . . . . . . . 43:1--43:??
Zachary Kincaid and
Nicolas Koh and
Shaowei Zhu When Less Is More: Consequence-Finding
in a Weak Theory of Arithmetic . . . . . 44:1--44:??
Mosaad Al Thokair and
Minjian Zhang and
Umang Mathur and
Mahesh Viswanathan Dynamic Race Detection with $ O(1) $
Samples . . . . . . . . . . . . . . . . 45:1--45:??
Swaraj Dash and
Younesse Kaddar and
Hugo Paquet and
Sam Staton Affine Monads and Lazy Structures for
Bayesian Programming . . . . . . . . . . 46:1--46:??
Zilin Chen and
Ambroise Lafont and
Liam O\textquotesingleConnor and
Gabriele Keller and
Craig McLaughlin and
Vincent Jackson and
Christine Rizkallah \pkgDargent: a Silver Bullet for
Verified Data Layout Refinement . . . . 47:1--47:??
Litao Zhou and
Yaoda Zhou and
Bruno C. d. S. Oliveira Recursive Subtyping for All . . . . . . 48:1--48:??
Azadeh Farzan and
Dominik Klumpp and
Andreas Podelski Stratified Commutativity in Verification
Algorithms for Concurrent Programs . . . 49:1--49:??
Jianlin Li and
Leni Ven and
Pengyuan Shi and
Yizhou Zhang Type-Preserving, Dependence-Aware Guide
Generation for Sound, Effective
Amortized Probabilistic Inference . . . 50:1--50:??
Victor Arrial and
Giulio Guerrieri and
Delia Kesner Quantitative Inhabitation for Different
Lambda Calculi in a Unifying Framework 51:1--51:??
Jules Jacobs and
Thorsten Wißmann Fast Coalgebraic Bisimilarity
Minimization . . . . . . . . . . . . . . 52:1--52:??
Abhishek Kr Singh and
Ori Lahav An Operational Approach to Library
Abstraction under Relaxed Memory
Concurrency . . . . . . . . . . . . . . 53:1--53:??
Tom J. Smeding and
Matthijs I. L. Vákár Efficient Dual-Numbers Reverse AD via
Well-Known Program Transformations . . . 54:1--54:??
Cinzia Di Giusto and
Davide Ferré and
Laetitia Laversa and
Etienne Lozes A Partial Order View of Message-Passing
Communication Models . . . . . . . . . . 55:1--55:??
Ria Das and
Joshua B. Tenenbaum and
Armando Solar-Lezama and
Zenna Tavares Combining Functional and Automata
Synthesis to Discover Causal Reactive
Programs . . . . . . . . . . . . . . . . 56:1--56:??
Kuen-Bang Hou (Favonia) and
Carlo Angiuli and
Reed Mullanix An Order-Theoretic Analysis of Universe
Polymorphism . . . . . . . . . . . . . . 57:1--57:??
Viktor Palmkvist and
Elias Castegren and
Philipp Haller and
David Broman Statically Resolvable Ambiguity . . . . 58:1--58:??
Paraschos Koutris and
Shaleen Deep The Fine-Grained Complexity of CFL
Reachability . . . . . . . . . . . . . . 59:1--59:??
Vasileios Klimis and
Jack Clark and
Alan Baker and
David Neto and
John Wickerson and
Alastair F. Donaldson Taking Back Control in an Intermediate
Representation for GPU Computing . . . . 60:1--60:??
Nicolas Chappe and
Paul He and
Ludovic Henrio and
Yannick Zakowski and
Steve Zdancewic Choice Trees: Representing
Nondeterministic, Recursive, and Impure
Programs in Coq . . . . . . . . . . . . 61:1--61:??
Casper Bach Poulsen and
Cas van der Rest Hefty Algebras: Modular Elaboration of
Higher-Order Algebraic Effects . . . . . 62:1--62:??
Francesco Gavazzo and
Cecilia Di Florio Elements of Quantitative Rewriting . . . 63:1--63:??
Filippo Bonchi and
Alessandro Di Giorgio and
Alessio Santamaria Deconstructing the Calculus of Relations
with Tape Diagrams . . . . . . . . . . . 64:1--64:??
Matthieu Lemerre SSA Translation Is an Abstract
Interpretation . . . . . . . . . . . . . 65:1--65:??
Ankush Das and
Di Wang and
Jan Hoffmann Probabilistic Resource-Aware Session
Types . . . . . . . . . . . . . . . . . 66:1--66:??
Kevin Batz and
Benjamin Lucien Kaminski and
Joost-Pieter Katoen and
Christoph Matheja and
Lena Verscht A Calculus for Amortized Expected
Runtimes . . . . . . . . . . . . . . . . 67:1--67:??
Sebastian Hunt and
David Sands and
Sandro Stucki Reconciling Shannon and Scott with a
Lattice of Computable Information . . . 68:1--68:??
Jerome Jochems and
Eddie Jones and
Steven Ramsay Higher-Order MSL Horn Constraints . . . 69:1--69:??
Woosuk Lee and
Hangyeol Cho Inductive Synthesis of Structurally
Recursive Functional Programs from
Non-recursive Expressions . . . . . . . 70:1--70:??
Taro Sekiyama and
Hiroshi Unno Temporal Verification with Answer-Effect
Modification: Dependent Temporal
Type-and-Effect System with Delimited
Continuations . . . . . . . . . . . . . 71:1--71:??
Hiroshi Unno and
Tachio Terauchi and
Yu Gu and
Eric Koskinen Modular Primal-Dual Fixpoint Logic
Solving for Temporal Verification . . . 72:1--72:??
Pascal Baumann and
Moses Ganardi and
Rupak Majumdar and
Ramanathan S. Thinniyam and
Georg Zetzsche Context-Bounded Verification of
Context-Free Specifications . . . . . . 73:1--73:??
Lo\"\ic Pujet and
Nicolas Tabareau Impredicative Observational Equality . . 74:1--74:??
Shaohua Li and
Zhendong Su Accelerating Fuzzing through
Prefix-Guided Execution . . . . . . . . 75:1--75:??
Chenglin Wang and
Fangzhen Lin Solving Conditional Linear Recurrences
for Program Verification: The Periodic
Case . . . . . . . . . . . . . . . . . . 76:1--76:??
Zhengyao Lin and
Xiaohong Chen and
Minh-Thai Trinh and
John Wang and
Grigore Ro\csu Generating Proof Certificates for a
Language-Agnostic Deductive Program
Verifier . . . . . . . . . . . . . . . . 77:1--77:??
Shraddha Barke and
Michael B. James and
Nadia Polikarpova Grounded Copilot: How Programmers
Interact with Code-Generating Models . . 78:1--78:??
Lorenzo Gheri and
Nobuko Yoshida Hybrid Multiparty Session Types:
Compositionality for Protocol
Specification through Endpoint
Projection . . . . . . . . . . . . . . . 79:1--79:??
Paul Krogmeier and
P. Madhusudan Languages with Decidable Learning: a
Meta-theorem . . . . . . . . . . . . . . 80:1--80:??
Christopher Wagner and
Nouraldin Jaber and
Roopsha Samanta Enabling Bounded Verification of
Doubly-Unbounded Distributed
Agreement-Based Systems via Bounded
Regions . . . . . . . . . . . . . . . . 81:1--81:??
Bo Wang and
Aashish Kolluri and
Ivica Nikoli\'c and
Teodora Baluta and
Prateek Saxena User-Customizable Transpilation of
Scripting Languages . . . . . . . . . . 82:1--82:??
Xing Zhang and
Guanchen Guo and
Xiao He and
Zhenjiang Hu Bidirectional Object-Oriented
Programming: Towards Programmatic and
Direct Manipulation of Objects . . . . . 83:1--83:??
Wenjia Ye and
Mat\'ìas Toro and
Federico Olmedo A Gradual Probabilistic Lambda Calculus 84:1--84:??
Andrea Lattuada and
Travis Hance and
Chanhee Cho and
Matthias Brun and
Isitha Subasinghe and
Yi Zhou and
Jon Howell and
Bryan Parno and
Chris Hawblitzel Verus: Verifying Rust Programs using
Linear Ghost Types . . . . . . . . . . . 85:1--85:??
Jie Zhou and
John Criswell and
Michael Hicks Fat Pointers for Temporal Memory Safety
of C . . . . . . . . . . . . . . . . . . 86:1--86:??
Chan Gu Kang and
Hakjoo Oh Modular Component-Based Quantum Circuit
Synthesis . . . . . . . . . . . . . . . 87:1--87:??
Anthony C. J. Fox and
Gareth Stockwell and
Shale Xiong and
Hanno Becker and
Dominic P. Mulligan and
Gustavo Petri and
Nathan Chong A Verification Methodology for the
Arm\reg Confidential Computing
Architecture: From a Secure
Specification to Safe Implementations 88:1--88:??
Jan Menz and
Andrew K. Hirsch and
Peixuan Li and
Deepak Garg Compositional Security Definitions for
Higher-Order Where Declassification . . 89:1--89:??
Yuval Shapira and
Eran Avneri and
Dana Drachsler-Cohen Deep Learning Robustness Verification
for Few-Pixel Attacks . . . . . . . . . 90:1--90:??
Ike Mulder and
Robbert Krebbers Proof Automation for Linearizability in
Separation Logic . . . . . . . . . . . . 91:1--91:??
Alexis Le Glaunec and
Lingkun Kong and
Konstantinos Mamouras Regular Expression Matching using Bit
Vector Automata . . . . . . . . . . . . 92:1--92:??
Noam Zilberstein and
Derek Dreyer and
Alexandra Silva Outcome Logic: a Unifying Foundation for
Correctness and Incorrectness Reasoning 93:1--93:??
Mehmet Emre and
Peter Boyland and
Aesha Parekh and
Ryan Schroeder and
Kyle Dewey and
Ben Hardekopf Aliasing Limits on Translating C to Safe
Rust . . . . . . . . . . . . . . . . . . 94:1--94:??
Guoqiang Zhang and
Benjamin Mariano and
Xipeng Shen and
I\csìl Dillig Automated Translation of Functional Big
Data Queries to SQL . . . . . . . . . . 95:1--95:??
Yongwei Yuan and
Scott Guest and
Eric Griffis and
Hannah Potter and
David Moon and
Cyrus Omar Live Pattern Matching with Typed Holes 96:1--96:??
Zhenyang Xu and
Yongqiang Tian and
Mengxiao Zhang and
Gaosen Zhao and
Yu Jiang and
Chengnian Sun Pushing the Limit of $1$-Minimality of
Language-Agnostic Program Reduction . . 97:1--97:??
David Chiang and
Colin McDonald and
Chung-chieh Shan Exact Recursive Probabilistic
Programming . . . . . . . . . . . . . . 98:1--98:??
Shenghua Feng and
Mingshuai Chen and
Han Su and
Benjamin Lucien Kaminski and
Joost-Pieter Katoen and
Naijun Zhan Lower Bounds for Possibly Divergent
Probabilistic Programs . . . . . . . . . 99:1--99:??
Amir Kafshdar Goharshady and
S. Hitarth and
Fatemeh Mohammadi and
Harshit Jitendra Motwani Algebro-geometric Algorithms for
Template-Based Synthesis of Polynomial
Programs . . . . . . . . . . . . . . . . 100:1--100:??
Levin N. Winter and
Florena Buse and
Daan de Graaf and
Klaus von Gleissenthall and
Burcu Kulahcioglu Ozkan Randomized Testing of Byzantine Fault
Tolerant Algorithms . . . . . . . . . . 101:1--101:??
Thibault Dardinier and
Gaurav Parthasarathy and
Peter Müller Verification-Preserving Inlining in
Automatic Separation Logic Verifiers . . 102:1--102:??
Ruyi Ji and
Chaozhe Kong and
Yingfei Xiong and
Zhenjiang Hu Improving Oracle-Guided Inductive
Synthesis by Efficient Question
Selection . . . . . . . . . . . . . . . 103:1--103:??
Marius Müller and
Philipp Schuster and
Jonathan Immanuel Brachthäuser and
Klaus Ostermann Back to Direct Style: Typed and Tight 104:1--104:??
Ori Roth and
Yossi Gil Fluent APIs in Functional Languages . . 105:1--105:??