Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Events (31 results)

A Limited Case for Reification by Type Inference

CoqPL When: Tue 19 Jan 2021 16:00 - 16:15 People: Jason Gross

… and interesting in its own right. This, after all, is how reification …

Causal-Consistent Reversible Debugging: Improving CauDEr

PADL 2021 When: Tue 19 Jan 2021 16:30 - 17:00 People: Juan José González-Abril, German Vidal

… , as long as all the actions that depend on the action we want to undo have been … framework, and develop a new version of the debugging tool CauDEr including all

Strictly Capturing Non-Strict Closures

PEPM 2021 When: Tue 19 Jan 2021 18:30 - 19:00 People: Zachary Sullivan, Paul Downen, Zena M. Ariola

All functional languages need closures. Closure-conversion is a compiler transformation that embeds static code for creating and manipulating closures into the program, avoiding the need to do this at run-time. For call-by-value …

A Self-Certifying Compilation Framework for WebAssembly

VMCAI When: Sun 17 Jan 2021 18:15 - 18:30 People: Kedar Namjoshi, Anton Xue

… for WebAssembly, a new intermediate language supported by all major browsers. …

Algebra-based Synthesis of Loops and their Invariants

VMCAI When: Mon 18 Jan 2021 16:00 - 17:00 People: Laura Kovacs, Andreas Humenberger

all polynomial equality invariants of such non-deterministic numeric single-path …

Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible

VMCAI When: Mon 18 Jan 2021 18:30 - 18:45 People: Marius Kamp, Michael Philippsen

… but also require a synthesizer to detect if there is no such program at all

Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories

VMCAI When: Tue 19 Jan 2021 18:30 - 18:45 People: Martin Bromberger, Alberto Fiori, Christoph Weidenbach

… inferences on the original clauses with variables. We prove that all clauses …

A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers

Lightning Talks When: Mon 18 Jan 2021 20:20 - 20:25 People: Sören Bleikertz, Andreas Lochbihler, Ognjen Marić, Simon Meier, Phoebe Nichols, Matthias Schmalz, Ratko G. Veprek

… running on a single blockchain, as it defines a total order on all transactions … protocol Canton supports atomic transactions across all these Daml … is respected even though individual system users cannot see all dependencies due …

An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR

CPP 2021 When: Tue 19 Jan 2021 17:00 - 17:15 People: Max W. Haslbeck, René Thiemann

… the generated proofs.· To this end, we require formal semantics of all program …

Gradualizing the Calculus of Inductive Constructions

Lightning Talks When: Mon 18 Jan 2021 20:10 - 20:15 People: Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter

… Triangle. We develop a parametrized presentation of Gradual CIC that encompasses all

Extracting Smart Contracts Tested and Verified in Coq

CPP 2021 When: Mon 18 Jan 2021 18:45 - 19:00 People: Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters

… private except under collusion of all other parties. With ConCert’s executable …

Invited Talk: Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures

CPP 2021 When: Mon 18 Jan 2021 16:00 - 17:00 People: Peter Sewell

… development.

All these tools and models are (or will soon be) available under open …

Petsy: Polymorphic Enumerative Type-Guided Synthesis

Student Research Competition People: Darya Verzhbinsky, Daniel Wang

… components in all experiments. When comparing Petsy with Tygar, Petsy, both tools …

A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis

POPL When: Wed 20 Jan 2021 18:50 - 19:00 People: Vineet Rajani, Marco Gaboardi, Deepak Garg, Jan Hoffmann

… of the embeddings also implies that λ-amor is relatively complete for all terminating PCF …

Mechanized Logical Relations for Termination-Insensitive Noninterference

POPL When: Thu 21 Jan 2021 16:10 - 16:20 People: Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal

… re-usable theory of Modal Weakest Preconditions. We formalize all of our theory …

Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic

POPL When: Fri 22 Jan 2021 16:25 - 16:35 People: Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal

… formalization of the Aneris logic to formalize all the results presented in the paper …

A Separation Logic for Effect Handlers

POPL When: Fri 22 Jan 2021 16:15 - 16:25 People: Paulo Emílio de Vilhena, François Pottier

… rule and a bind rule. It is based on Iris and inherits all of its advanced …

A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types

POPL When: Wed 20 Jan 2021 16:00 - 16:10 People: Chao-Hong Chen, Amr Sabry

… . The operational semantics, most of its meta-theoretic properties, and all examples …

An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants

POPL When: Wed 20 Jan 2021 18:50 - 19:00 People: Jay P. Lim, Mridul Aanjaneya, John Gustafson, Santosh Nagarakatte

… correctly rounded results for all inputs. We frame the problem of generating …

An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs

POPL When: Wed 20 Jan 2021 19:00 - 19:10 People: Julian Rosemann, Simon Moll, Sebastian Hack

… Vectorizing compilers employ divergence analysis to detect at which program point a specific variable is uniform, i.e. has the same value on all SIMD threads that execute this program point. They exploit uniformity to retain branching …

Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification

POPL When: Wed 20 Jan 2021 19:10 - 19:20 People: Cameron Moy, Phúc C. Nguyễn, Sam Tobin-Hochstadt, David Van Horn

… program to prove that almost all of the dynamic checks implied by gradual …

Internalizing Representation Independence with Univalence

POPL When: Wed 20 Jan 2021 16:10 - 16:20 People: Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner

… by considering applications to matrices, queues, and finite multisets. Our results are all

On the Semantic Expressiveness of Recursive Types

POPL When: Thu 21 Jan 2021 18:40 - 18:50 People: Marco Patrignani, Eric Mark Martin, Dominique Devriese

… -typed interface. The three proofs all rely on a typed version of a proof technique …

Toward a Programmable Cloud: CALM Foundations and Open Challenges

POPL When: Fri 22 Jan 2021 17:00 - 18:00 People: Joseph M. Hellerstein

… Major shifts in computing platforms are often accompanied by new programming models. The public cloud emerged a decade ago, but we have yet to see a new generation of programming platforms adopted in response. All the traditional …

Fully Abstract from Static to Gradual

POPL When: Wed 20 Jan 2021 16:00 - 16:10 People: Koen Jacobs, Amin Timany, Dominique Devriese

… that all source language equivalences are preserved. We demonstrate …

Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade

POPL When: Thu 21 Jan 2021 16:40 - 16:50 People: Marco Vassena, Craig Disselkoen, Klaus v. Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, Deian Stefan

… that all sink expressions are stable. Blade relies on a new new abstract …

Intrinsically Typed Compilation with Nameless Labels

POPL When: Wed 20 Jan 2021 16:10 - 16:20 People: Arjen Rouvoet, Robbert Krebbers, Eelco Visser

… * to ensure that all labels are defined exactly once. To write concise compilers …

Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion

POPL When: Thu 21 Jan 2021 18:30 - 18:40 People: Patrick Bahr, Christian Uldal Graulund, Rasmus Ejlers Møgelberg

… When designing languages for functional reactive programming (FRP) the main challenge is to provide the user with a simple, flexible interface for writing programs on a high level of abstraction while ensuring that all programs can …

Precise Subtyping for Asynchronous Multiparty Sessions

POPL When: Fri 22 Jan 2021 16:05 - 16:15 People: Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, Nobuko Yoshida

… relation must capture all such valid permutations — and consequently, its …

Deciding Accuracy of Differential Privacy Schemes

POPL When: Fri 22 Jan 2021 15:55 - 16:05 People: Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan

… is the minimal distance d(x, y) over all y such that f(y) ≠ f(x …

λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes

POPL When: Fri 22 Jan 2021 15:45 - 15:55 People: Benjamin Sherman, Jesse Michel, Michael Carbin

… distributions, implicit surfaces, and generalized parametric surfaces — all