Events (53 results)

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 …

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 …

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 …

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 …

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

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 …

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 …

Simplifying Concurrent Programming via Synchronization Synthesis

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 …

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 …

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 …

(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

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 …

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 …

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 …

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 …

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

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

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 …

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 …

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 …

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 …

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

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 …

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

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 …

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 …

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 …