## Search *events* for 'all'

#### Partially Evaluating Symbolic Interpreters for All

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

… …

#### Position Paper: LLD is All You Need

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

… …

#### Towards Understanding Spectre-PHT in Memory-Safe Languages

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 …

#### Proving and Programming

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 …

#### Scrap your boilerplate definitions in 10 lines of Ltac!

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 …

#### From meta frameworks and transformations to distributed computing and more

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 …

#### let (rec) insertion without Effects, Lights or Magic

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 …

#### Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages

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 …

#### SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation

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 …

#### Littleton: An Educational Environment for Property Law

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 …

#### Type-aware equational rewriting (discussion)

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 …

#### DPCL: a Language Template for Normative Specifications

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 …

#### Gotta prove fast: building an ecosystem for effortless native compilation of tactics

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 …

#### Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting

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 …

#### Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata

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 …

#### Coq’s vibrant ecosystem for verification engineering

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 …

#### Benchmarking Binding (discussion)

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 …

#### mitten: A Flexible Multimodal Proof Assistant

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 …

#### Implementing a category-theoretic framework for typed abstract syntax

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 …

#### Certified Abstract Machines for Skeletal Semantics

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 …

#### A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem

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

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

#### Simplifying Concurrent Programming via Synchronization Synthesis

VMCAI 2022 **When: **Tue 18 Jan 2022 13:30 - 14:30 **People: **Işil Dillig

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

#### Typechecking up to Congruence

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 …

#### Tries that match

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 …

#### (Deep) Induction Rules for GADTs

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 …

#### Forward build systems, formally

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 …

#### Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking

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 …

#### Sequential Information Flow

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 …

#### Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives

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. …

#### Applying Formal Verification to Microkernel IPC at Meta

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 …

#### One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes

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 …

#### Fair Termination of Binary Sessions

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 …

#### Effectful Program Distancing

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 …

#### Pirouette: Higher-Order Typed Functional Choreographies

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

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

#### Property-Directed Reachability as Abstract Interpretation in the Monotone Theory

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 …

#### Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis

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 …

#### Efficient Algorithms for Dynamic Bidirected Dyck-Reachability

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 …

#### Visibility Reasoning for Concurrent Snapshot Algorithms

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 …

#### Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites

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 …

#### Subcubic Certificates for CFL Reachability

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. …

#### From Enhanced Coinduction towards Enhanced Induction

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 …

#### Truly Stateless, Optimal Dynamic Partial Order Reduction

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 …

#### A Relational Theory of Effects and Coeffects

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 …

#### Static Prediction of Parallel Computation Graphs

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 …

#### Gradualizing the Calculus of Inductive Constructions

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 …

#### On Incorrectness Logic and Kleene Algebra with Top and Tests

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 …

#### A Dual Number Abstraction for Static Analysis of Clarke Jacobians

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 …

#### A Cost-Aware Logical Framework

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 …

#### Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI

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 …

#### Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations

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 …

#### Safe, Modular Packet Pipeline Programming

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 …

#### A Formal Foundation for Symbolic Evaluation with Merging

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 …

#### The Decidability and Complexity of Interleaved Bidirected Dyck Reachability

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 …