Search events for 'all'
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
λ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 …
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 …
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 …