PEPM 2022 When: Mon 17 Jan 2022 11:35 - 12:05 People: Shangyin Tan, Guannan Wei, Tiark Rompf

… …

ProLaLa Programming Languages and the Law When: Sun 16 Jan 2022 10:20 - 10:40 People: L. Thorne McCarty

… …

PriSC 2022 When: Sat 22 Jan 2022 10:45 - 11:10 People: Zirui Neil Zhao, Fangfei Liu, Scott Constable, Carlos Rozas

… , memory safety techniques cannot stop all Spectre-PHT variants, since not all … to defend against all Spectre-PHT variants with low execution overhead. Therefore …

PLMW 2022 When: Tue 18 Jan 2022 15:05 - 15:40 People: Zena M. Ariola

… implementations. But most of all, it emphasizes that it doesn’t matter if you …

CoqPL When: Sat 22 Jan 2022 10:40 - 11:00 People: Qianchuan Ye, Benjamin Delaware

… , powered by Template-Coq and using Ltac to do all the heavy lifting. We give several …

PEPM 2022 When: Mon 17 Jan 2022 12:55 - 13:55 People: Y. Annie Liu

… . All these further propelled the study of logic and constraints, the foundation …

PEPM 2022 When: Tue 18 Jan 2022 06:05 - 06:35 People: Oleg Kiselyov, Jeremy Yallop

… (rec)-insertion, which does not rely on any effects at all. The formalization …

LAFI When: Sun 16 Jan 2022 15:05 - 15:23 People: Alexander K. Lew, Mathieu Huot, Vikash K. Mansinghka

… or recursion) holds: all programs denote so-called omega-PAP functions, and AD …

PriSC 2022 When: Sat 22 Jan 2022 15:30 - 15:55 People: Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Cătălin Hriţcu, Deepak Garg

… the generated attacker had to stash all reachable pointers.

In this work, we …

ProLaLa Programming Languages and the Law When: Sun 16 Jan 2022 13:30 - 13:40 People: Shrutarshi Basu, Anshuman Mohan, James Grimmelmann, Nate Foster

… and a complete set of examples, all packaged into an easily deployable web-based …

WITS 2022 When: Sat 22 Jan 2022 09:15 - 10:00 People: Richard A. Eisenberg

… computation, and we have come up with an algorithm that (we believe) handles all …… and maybe they’re all different! This discussion will be about sharing and discussing …

ProLaLa Programming Languages and the Law When: Sun 16 Jan 2022 11:20 - 11:40 People: Giovanni Sileno, Thomas van Binsbergen, Matteo Pascucci, Tom van Engers

… been identified enabling us to easily compare them. Yet, all these efforts share … it is plausible that there may be a representational model encompassing all of them …

WITS 2022 When: Sat 22 Jan 2022 13:45 - 14:00 People: Sebastian Ullrich

… We report on ongoing work on bringing automatic, zero-setup native compilation of Lean metaprograms including tactics to Lean 4. A core component is a self-contained compilation toolchain based on LLVM for all major platforms supported …

CPP 2022 When: Tue 18 Jan 2022 10:45 - 11:10 People: Michael Färber

… either does not support concurrency at all or only limited forms thereof … checker for this calculus, Dedukti, on all of five evaluated datasets obtained …

VMCAI 2022 When: Tue 18 Jan 2022 15:35 - 16:05 People: Yuming Wu, Lei Bu, Jiawan Wang, Xinyue Ren, Wen Xiong, Xuandong Li

… in the discrete layer of CLHA through the classical step semantics. Then, we remove all stutter transitions in the candidate paths to cover all interleaving cases …

CPP 2022 When: Mon 17 Jan 2022 09:00 - 10:00 People: Andrew W. Appel

… mechanized proof theories from many domains, and they must all interoperate …

WITS 2022 When: Sat 22 Jan 2022 15:05 - 15:20 People: Philipp Stassen, Daniel Gratzer, Lars Birkedal

… proof assistant implementing these algorithms which supports all decidable …

WITS 2022 When: Sat 22 Jan 2022 14:00 - 14:45 People: Stephanie Weirich

… Implementations of type systems, logics and programming languages must often answer the question of how to represent and work with binding structures in terms. While there may not be a one-size-fits-all solution, I would like …

CPP 2022 When: Tue 18 Jan 2022 16:30 - 16:55 People: Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

… notion of strong functors between actions, all formalized in UniMath using a recently … to plug all of these ingredients together, modularly.

The main result of our work …

CPP 2022 When: Mon 17 Jan 2022 11:35 - 12:00 People: Guillaume Ambal, Sergueï Lenglet, Alan Schmitt

… machines. All these interpretations are formalized in the Coq proof assistant …

CPP 2022 When: Tue 18 Jan 2022 14:45 - 15:10 People: Ariel E. Kellison

… show, going back to the axioms, that all of the auxiliary theorems used are also …

VMCAI 2022 When: Tue 18 Jan 2022 13:30 - 14:30 People: Işıl Dillig

… -by-construction. Our method infers all signaling operations that are needed …

WITS 2022 When: Sat 22 Jan 2022 15:50 - 16:05 People: Jad Elkhaleq Ghalayini

… In Programming up to Congruence, Sjöberg and Weirich handle potentially nonterminating terms by taking the somewhat radical step of designing a dependently typed language not equipped with automatic β-reduction at all, instead using …

WITS 2022 When: Sat 22 Jan 2022 13:30 - 13:45 People: Sebastian Graf

… the index retrieves all (pattern,value) pairs of which the query term …

CPP 2022 When: Mon 17 Jan 2022 16:45 - 17:10 People: Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt

… } or \textsc{Memoize}, are also correct.

We carry out all of our work in Agda …

CPP 2022 When: Tue 18 Jan 2022 16:55 - 17:20 People: Patricia Johann, Enrico Ghiorzi

… Deep data types are those that are constructed from other data types, including, possibly, themselves. In this case, they are said to be truly nested. Deep induction is an extension of structural induction that traverses {\em all …

VMCAI 2022 When: Sun 16 Jan 2022 09:00 - 10:00 People: Thomas A. Henzinger

… variants of sequential information flow, including all variants in which …

VMCAI 2022 When: Mon 17 Jan 2022 10:20 - 10:50 People: Peter Gjøl Jensen, Jiri Srba, Nikolaj Jensen Ulrik, Simon Mejlby Virenfeldt

… In LTL model checking, a system model is synchronized using the product construction with Buchi automaton representing all runs that invalidate a given LTL formula. An existence of a run with infinitely many occurrences of an accepting …

CPP 2022 When: Mon 17 Jan 2022 13:55 - 14:20 People: Derek Egolf, Sam Lasser, Kathleen Fisher

… types. All extensions were implemented and verified with the Coq Proof Assistant. …

CPP 2022 When: Mon 17 Jan 2022 11:10 - 11:35 People: Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli

… atomic load, and one boolean check, all in a performance-sensitive part of the OS …

POPL When: Fri 21 Jan 2022 17:05 - 17:30 People: Jay P. Lim, Santosh Nagarakatte

… rounded results for all inputs. In contrast, CR-LIBM and RLIBM provide correctly … that produces correctly rounded results for all inputs for multiple rounding modes … results for all five rounding modes in the standard and for multiple representations …

POPL When: Fri 21 Jan 2022 10:45 - 11:10 People: Luca Ciccone, Luca Padovani

… sessions. A session fairly terminates if all of the infinite executions admitted … assumptions*. Fair termination entails the eventual completion of all pending … carefully account for all usages of fair subtyping to avoid compromising its …

POPL When: Fri 21 Jan 2022 14:20 - 14:45 People: Ugo Dal Lago, Francesco Gavazzo

… Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are \emph{not} equivalent are treated the same, and simply … for a new contextual form of reasoning. In this paper, we show that all this can …

POPL When: Fri 21 Jan 2022 10:20 - 10:45 People: Andrew K. Hirsch, Deepak Garg

… . All of our results are verified in Coq. …

POPL When: Wed 19 Jan 2022 13:30 - 13:55 People: Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox

… , called $\Lambda$-PDR, in which all generalizations of a counterexample are used … their creation, because all the possible supporting facts are included in advance …

POPL When: Wed 19 Jan 2022 13:55 - 14:20 People: Marco Campion, Mila Dalla Preda, Roberto Giacobazzi

… verification. As all alarming systems, a program analysis tool is credible when few false … alarms, but also we need methods to control them.
As for all approximation …

POPL When: Wed 19 Jan 2022 15:05 - 15:30 People: Yuanbo Li, Kris Satya, Qirun Zhang

… \emph{all-pairs} reachability information in $O(m)$ time.

This paper focuses … consider the problem of maintaining all-pairs Dyck-reachability information … to achieve $O(1)$ query time. All-pairs Dyck-reachability is a generalization …

POPL When: Wed 19 Jan 2022 15:05 - 15:30 People: Joakim Öhman, Aleksandar Nanevski

… the components at higher abstraction levels are shared, i.e., they apply to all …

POPL When: Fri 21 Jan 2022 16:40 - 17:05 People: Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley

… for compilation targeting imperative code with arrays and nested loops, all rewrites …

POPL When: Wed 19 Jan 2022 15:55 - 16:20 People: Dmitry Chistikov, Rupak Majumdar, Philipp Schepper

… reachability and 2NPDA recognition; as well as to all-pairs CFL reachability … core'' of all these problems. …

POPL When: Wed 19 Jan 2022 15:55 - 16:20 People: Stefan K. Muller

… graph types, which compactly represent all of the graphs that could arise from …

POPL When: Fri 21 Jan 2022 13:55 - 14:20 People: Ugo Dal Lago, Francesco Gavazzo

… of a relator) is precisely what is needed to prove all the aforementioned program …

POPL When: Fri 21 Jan 2022 10:20 - 10:45 People: Davide Sangiorgi

… ones. We consider both strong semantics (in which all actions are treated equally …

POPL When: Thu 20 Jan 2022 10:20 - 10:45 People: Jacob Laurel, Rem Yang, Gagandeep Singh, Sasa Misailovic

… , adapted to soundly over-approximate all first derivatives needed to compute the Clarke …

POPL When: Fri 21 Jan 2022 14:20 - 14:45 People: Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter

… develop a parametrized presentation of Gradual CIC (GCIC) that encompasses all …

POPL When: Wed 19 Jan 2022 11:35 - 12:00 People: Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi

… to express a codomain operation, to express incorrectness triples, and to prove all …

POPL When: Wed 19 Jan 2022 14:20 - 14:45 People: Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis

… Dynamic partial order reduction (DPOR) verifies concurrent programs by exploring all their interleavings up to some equivalence relation, such as Mazurkiewicz trace equivalence. Doing so involves a complex trade-off between space …

POPL When: Fri 21 Jan 2022 11:10 - 11:35 People: Devon Loehr, David Walker

… their programs to compile to specialized networking hardware. In particular, all …

POPL When: Fri 21 Jan 2022 15:05 - 15:30 People: Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper

… } complexity of merge sort, all fully mechanized in the Agda proof assistant …

POPL When: Thu 20 Jan 2022 13:30 - 13:55 People: Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak

… Reusable symbolic evaluators are a key building block of solver-aided verification and synthesis tools. A reusable evaluator reduces the semantics of all paths in a program to logical constraints, and a client tool uses these constraints …

POPL When: Wed 19 Jan 2022 10:45 - 11:10 People: Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer

… of loop bodies), or has treated all synchronization operations as external …

POPL When: Thu 20 Jan 2022 15:05 - 15:30 People: Matthew Kolosick, Shravan Ravi Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan

… unexplored: almost all SFI systems use \emph{heavyweight transitions …

POPL When: Wed 19 Jan 2022 15:30 - 15:55 People: Adam Husted Kjelstrøm, Andreas Pavlogiannis

… the decidability and complexity of all variants of interleaved bidirected Dyck …