Search events for 'all'
Functorial Syntax for All
CoqPL 2024 When: Sat 20 Jan 2024 14:22 - 14:45 People: Piotr Polesiuk, Filip Sieczkowski
… …
All the Binaries Together: A Semantic Approach to Application Binary Interfaces
PriSC 2024 When: Sat 20 Jan 2024 14:45 - 15:07 People: Andrew Wagner, Amal Ahmed
… Nearly all modern systems critically depend on interoperability between languages and libraries, but reasoning formally about this interaction has proven … machinery slowly disappears, and all that remains is an unspoken promise between …
Quotient Haskell: Lightweight Quotient Types for All
POPL When: Thu 18 Jan 2024 10:50 - 11:10 People: Brandon Hewer, Graham Hutton
… …
QGAT: A Generate-and-Test Paradigm for Quantum Circuits
PLanQC 2024 When: Sat 20 Jan 2024 17:07 - 17:30 People: Ulrik de Muelenaere
… all the possible solutions for a problem and tests them for the “best … that the underlying classical intuition is all that is needed to express and understand common …
How to Give a Talk
PLMW @ POPL 2024 When: Tue 16 Jan 2024 16:00 - 16:45 People: Neel Krishnaswami
… In this talk, I will discuss both why we give scientific talks at all, and also how to structure effective scientific presentations. I’ll focus primarily on how to structure your talk to help the audience understand it, and will also spend …
Work in Progress: Modelling Incorrect Programs in the Open World with Dafny
Incorrectness When: Tue 16 Jan 2024 11:45 - 12:07 People: James Noble, Tobias Wrigstad, Susan Eisenbach
… Software verification typically assumes a “closed world”: that all modules of a system can be verified, or at least the provenance of all the modules can be assured. Real systems, however, have to interact with the “open world”: third …
Generating Executable Specification from Formal Semantics of WebAssembly
WAW 2024 When: Mon 15 Jan 2024 14:45 - 15:30 People: Sukyoung Ryu
… reduce errors, manually generating all the artifacts is labor intensive and error …
Efficient Evaluation with Controlled Definition Unfolding
WITS 2024 When: Sat 20 Jan 2024 16:30 - 17:00 People: András Kovács
… if definitions are unfolded all the time. Additionally, conversion checking and scope …
Heterogeneous concurrency -- a new frontier for weak memory
The Future of Weak Memory 2024 When: Mon 15 Jan 2024 09:30 - 09:50 People: Soham Chakraborty
… Heterogeneous processors that combine different types of processors such as CPUs, GPUs, and accelerators are emerging in all domains of computing. The state-of-the-art of these heterogeneous processors is advancing faster than ever …
Normal Form Bisimulations by Value
GALOP 2024 When: Sun 14 Jan 2024 09:45 - 10:07 People: Beniamino Accattoli, Adrienne Lancelot, Claudia Faggian
… Sangiorgi’s normal form bisimilarity is call-by-name, identifies all the call-by-name meaningless terms, and rests on open terms in its definition …, Lassen’s enf bisimilarity, which validates all of Moggi’s monadic laws. The starting …
Ill-Typed Programs Don't Evaluate
Incorrectness When: Tue 16 Jan 2024 16:23 - 16:45 People: Steven Ramsay, Charlie Walpole
… . By incorporating a type of all values, these type systems support more refined notions …
A Reachability Logic for a Weak Memory Model with Promises
Incorrectness When: Tue 16 Jan 2024 14:22 - 14:45 People: Lara Bargmann, Brijesh Dongol, Heike Wehrheim
… are underapproximating, since the set of all valid promises are not known at the start …
Type inference for application spines
WITS 2024 When: Sat 20 Jan 2024 12:00 - 12:30 People: Simon Peyton Jones
… application spines all at once, thus f e1 e2 .. en.
I will describe a number …
A feasible and unitary programming language with quantum control
PLanQC 2024 When: Sat 20 Jan 2024 14:00 - 14:22 People: Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux, Mário Silva
… modalities: quantum circuit programs uphold unitarity, and all programs are evaluated …
Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abstract)
PLanQC 2024 When: Sat 20 Jan 2024 10:07 - 10:29 People: Andrea Colledan, Ugo Dal Lago
… Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all …
Incremental Computation: What Is the Essence? (Invited Contribution)
PEPM 2024 When: Tue 16 Jan 2024 17:30 - 18:00 People: Y. Annie Liu
… Incremental computation aims to compute more efficiently on changed input
by reusing previously computed results.
We give a high-level overview of works on incremental computation,
and highlight the essence underlying all of them …
Integrating Dependency Building with Document Checking in Coq
CoqPL 2024 When: Sat 20 Jan 2024 16:45 - 17:07 People: Emilio Jesús Gallego Arias, Bhakti Shah
… Coq users. On the performance front, we can share .vo file parsing among all …
Modularizing CPU Semantics for Virtualization
PriSC 2024 When: Sat 20 Jan 2024 14:22 - 14:45 People: Paolo G. Giarrusso, Abhishek Anand, Gregory Malecha, František Farka, Hoang-Hai Dang
… backwards simulation on the processor semantics would require case distinction on all …
When Obfuscations Preserve Cryptographic Constant-Time
PriSC 2024 When: Sat 20 Jan 2024 12:07 - 12:30 People: Matteo Busi, Pierpaolo Degano, Letterio Galletta
… for all possible programs, or the proof is too hard, we propose a translation …
QbC: Quantum Correctness by Construction
PLanQC 2024 When: Sat 20 Jan 2024 16:22 - 16:45 People: Anurudh Peduri, Ina Schaefer, Michael Walter
… programs using proof systems such as quantum Hoare logic. All these prior approaches …
Compilers should get over themselves and respect semantic dependencies!
The Future of Weak Memory 2024 When: Mon 15 Jan 2024 14:00 - 14:20 People: Paul E. McKenney
… , overly complex, or unloved by compiler implementers, and mostly all three …
Complete Stream Fusion for Software-Defined Radio
PEPM 2024 When: Tue 16 Jan 2024 11:00 - 11:25 People: Tomoaki Kobayashi, Oleg Kiselyov
… -written state machines. It guarantees complete
stream fusion in all cases …
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC 2024 When: Sat 20 Jan 2024 16:00 - 16:22 People: Robert Künnemann, Ethan Cecchetti
… . Finally, all proofs of the framework itself are verified in Isabelle/HOL. …
The Never-Ending Trace: An Under-Approximate Approach to Divergence Bugs
Incorrectness When: Tue 16 Jan 2024 11:22 - 11:45 People: Caroline Cronjäger
… divergence bugs and is under-approximating in the sense that all specified bugs …
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Dafny 2024 When: Sun 14 Jan 2024 10:12 - 10:30 People: Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
… properties for all the relevant stations. We present a simplified case study …
Why Languages Should Preserve Load-Store Order
The Future of Weak Memory 2024 When: Mon 15 Jan 2024 12:07 - 12:30 People: Stephen Dolan
… to varying degrees, but all are more complex than a programmer might expect …
Productivity Verification for Functional Programs by Reduction to Termination Verification
PEPM 2024 When: Tue 16 Jan 2024 10:05 - 10:30 People: Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato
… A program generating a co-inductive data structure is called productive if the program eventually generates all the elements of the data structure. We propose a new method for verifying the productivity, which transforms a co-inductive …
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
CPP 2024 When: Mon 15 Jan 2024 15:00 - 15:30 People: Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann
… generalize all mentioned criteria from confluence to commutation and integrate …
Modular Higher-Order Effects
PADL 2024 When: Mon 15 Jan 2024 09:00 - 10:00 People: Nicolas Wu
… —that is, algebraicity—is also their limitation: not all operations …
What we learned from C++ atomics and memory model standardization
The Future of Weak Memory 2024 When: Mon 15 Jan 2024 11:45 - 12:07 People: Hans-J. Boehm
… followed by all compilers on a system for all programming languages. Later evolution …
Verifying a concurrent file system with sequential reasoning
Dafny 2024 When: Sun 14 Jan 2024 09:10 - 10:10 People: Tej Chajed
… Bugs in systems software like file systems, databases, and operating systems can have serious consequences, ranging from security vulnerabilities to data loss, and these bugs affect all the applications built on top.
In this talk, I’ll …
Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Arguments
CPP 2024 When: Mon 15 Jan 2024 17:00 - 17:30 People: Joseph Eremondi
… with the same signatures as Brouwer tree constructors, and they satisfy all Brouwer … an infinite number of times. All definitions and theorems are implemented in Agda. …
Toward Probabilistic Coarse-to-Fine Program Synthesis
LAFI 2024 When: Sun 14 Jan 2024 15:00 - 15:10 People: Maddy Bowers, Alexander K. Lew, Vikash K. Mansinghka, Joshua B. Tenenbaum, Armando Solar-Lezama
… \textit{all} of the stochastic primitives; or alternatively, synthesis can …
Belief Programming in Partially Observable Probabilistic Environments
LAFI 2024 When: Sun 14 Jan 2024 11:20 - 11:30 People: Tobias Gürtler, Benjamin Lucien Kaminski
… belief program dynamically updates a probability distribution over all possible …
Formalizing the ∞-categorical Yoneda lemma
CPP 2024 When: Tue 16 Jan 2024 12:00 - 12:30 People: Nikolai Kudasov, Emily Riehl, Jonathan Weinberger
… is determined by its relationship to all of the other objects of the category. A key …
Displayed Monoidal Categories for the Semantics of Linear Logic
CPP 2024 When: Tue 16 Jan 2024 11:00 - 11:30 People: Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
… We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant.
All the categorical structures …
Dafny Test Generation
Dafny 2024 When: Sun 14 Jan 2024 11:00 - 11:18 People: Aleksandr Fedchin, Jeffrey S. Foster, Zvonimir Rakamaric, Aaron Tomb
… techniques that can fall short in scenarios like this when simple enumeration of all …
Resilience and Home-Space for WSTS
VMCAI 2024 When: Mon 15 Jan 2024 16:40 - 17:00 People: Alain Finkel, Mathieu Hilaire
… that most of all resilience problems are undecidable for WSTS with strong … all known WSTS are in this class) and Safe =↑ Safe. Moreover, some resilience …
Verification of Neural Networks’ Local Differential Classification Privacy
VMCAI 2024 When: Tue 16 Jan 2024 15:00 - 15:20 People: Roie Reshef, Anan Kabaha, Olga Seleznova, Dana Drachsler Cohen
… if it classifies all inputs the same regardless of whether it is trained … propose Sphynx, an algorithm that computes an abstraction of all networks …
Interpolation and Quantifiers in Ortholattices
VMCAI 2024 When: Mon 15 Jan 2024 10:05 - 10:25 People: Sankalp Gambhir, Simon Guilloud, Viktor Kunčak
… and complete for the class of all complete ortholattices. We show …
Towards a Categorical Model of the Lilac Separation Logic
LAFI 2024 When: Sun 14 Jan 2024 14:50 - 15:00 People: John Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, Steven Holtzen
… does not mention product spaces at all; rather, independent combination …
Boosting Constrained Horn Solving by Unsat Core Learning
VMCAI 2024 When: Mon 15 Jan 2024 11:20 - 11:40 People: Parosh Aziz Abdulla, Chencheng Liang, Philipp Rümmer
… results from a uniform selection of benchmarks across all categories from CHC …
Polyregular functions on unordered trees of bounded height
POPL When: Thu 18 Jan 2024 15:30 - 15:50 People: Mikolaj Bojanczyk, Bartek Klin
… on prime functions and combinators, which derives all first-order interpretations … that have bounded tree-depth. In all cases studied in this paper, first-order logic and MSO have the same expressive power, and hence all results apply also …
Reachability in Continuous Pushdown VASS
POPL When: Thu 18 Jan 2024 16:30 - 16:50 People: A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
… in NEXPTIME even if all numbers are specified in binary. On the other hand … stack, and even if all numbers are specified in unary. …
DEI4Everyone Reception
Diversity, Equity and Inclusion When: Thu 18 Jan 2024 18:30 - 20:00
… The reception will feature short talks from DEI representatives reflecting on their experiences around DEI issues. The event is open to everyone and our goal is to foster DEI discussions, all while drinking fabulous cocktails …
The Logical Essence of Well-Bracketed Control Flow
POPL When: Wed 17 Jan 2024 15:30 - 15:50 People: Amin Timany, Armaël Guéneau, Lars Birkedal
… all used involved relational models with explicit state-transition systems … relations models based on this program logic. All results presented in this paper …
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL When: Wed 17 Jan 2024 16:50 - 17:10 People: Pu Sun, Fu Song, Yuqi Chen, Taolue Chen
… -life cryptographic primitives including all the 10 finalists of the NIST … against differential cryptanalysis for all cryptographic primitives under …
Efficient Bottom-Up Synthesis for Programs with Local Variables
POPL When: Wed 17 Jan 2024 11:10 - 11:30 People: Xiang Li, Xiangyu Zhou, Rui Dong, Yihong Zhang, Xinyu Wang
… , from evaluating one program at a time to simultaneously evaluating all … enumerate all binding contexts for local variables, thereby enabling us …
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
POPL When: Fri 19 Jan 2024 10:30 - 10:50 People: John Cyphert, Zachary Kincaid
… to generate all polynomial invariants for a restricted class of programs. However … generate all polynomial invariants for arbitrary programs, our method establishes …
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL When: Fri 19 Jan 2024 17:30 - 17:50 People: Patrick Cousot
… of the semantics. As an example, we extend Hoare logic to cover all possible behaviors …
Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime
Student Research Competition When: Wed 17 Jan 2024 19:26 - 19:31 People: Jan-Paul Ramos-Davila
… checks for all imprecise logic, even if these formulas might share the same … and minimizing these common traces. We accomplish this by treating all iso … representation. By unrolling all static predicates as if they were dynamic checks …
Ill-Typed Programs Don't Evaluate
POPL When: Wed 17 Jan 2024 11:30 - 11:50 People: Steven Ramsay, Charlie Walpole
… formulas. By incorporating a type of all values, these type systems support …
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
POPL When: Wed 17 Jan 2024 16:50 - 17:10 People: Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, Lizzie Hernandez Videa
… object. All three of these proofs are machine-verified by TLAPS (the Temporal …
Effect handlers in Zig (extended abstract)
Student Research Competition When: Wed 17 Jan 2024 18:48 - 18:53 People: Alessio Duè
… the realization of an effect system that ensures that all effects are handled …
Modular Denotational Semantics for Effects with Guarded Interaction Trees
POPL When: Thu 18 Jan 2024 10:00 - 10:20 People: Daniel Frumin, Amin Timany, Lars Birkedal
… with different effects. All results in the paper are formalized in Coq using …
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL When: Thu 18 Jan 2024 14:40 - 15:00 People: Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers
… relations. All our results and examples have been mechanized in Coq. …
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL When: Fri 19 Jan 2024 15:50 - 16:10 People: Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao
… for all compiler passes into this Kripke Memory Relation and by piggybacking … compilation processes. Such direct refinements support all …
Pipelines and Beyond: Graph Types for ADTs with Futures
POPL When: Thu 18 Jan 2024 15:30 - 15:50 People: Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, Stefan K. Muller
… to a program by a type system and compactly represent the family of all graphs … forms of pipelining to achieve performance not attainable without futures. All …
Coarser Equivalences for Causal Concurrency
POPL When: Wed 17 Jan 2024 17:50 - 18:10 People: Azadeh Farzan, Umang Mathur
… they always appear in the same order in all equivalent runs). The same problem ….
Note: All missing proofs have been submitted as an anonymous supplementary …
Efficient CHAD
POPL When: Fri 19 Jan 2024 15:10 - 15:30 People: Tom Smeding, Matthijs Vákár
… to differentiating parallel functional programs: the key observations are 1) that all …
On Model-Checking Higher-Order Effectful Programs
POPL When: Thu 18 Jan 2024 09:00 - 09:20 People: Ugo Dal Lago, Alexis Ghyselen
… at the problem, first of all showing that there is an elegant and natural way …
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
POPL When: Thu 18 Jan 2024 11:10 - 11:30 People: Francesca Randone, Luca Bortolussi, Emilio Incerto, Mirco Tribastone
… Computing the posterior distribution of a probabilistic program is a hard task for which no one-fit-for-all solution exists. We propose Gaussian Semantics, which approximates the exact probabilistic semantics of a bounded program by means …
Zero-Cost Capabilities: Retrofitting Effect Safety in Rust
Student Research Competition When: Wed 17 Jan 2024 19:55 - 20:00 People: George Berdovskiy
… conducted two case studies porting popular Rust crates walkdir and `remove_dir_all …
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
POPL When: Wed 17 Jan 2024 15:50 - 16:10 People: Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
… on a number of case studies.
All the results that appear in the paper have …
DisLog: A Separation Logic for Disentanglement
POPL When: Thu 18 Jan 2024 16:10 - 16:30 People: Alexandre Moine, Sam Westrick, Stephanie Balzer
… hashing. All our results are mechanized in the Coq proof assistant using Iris. …
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
POPL When: Fri 19 Jan 2024 13:20 - 13:40 People: Lionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, Chun Yin Chau
… than all first-class-polymorphic type inference systems proposed so far …
How Hard is Weak-Memory Testing?
POPL When: Thu 18 Jan 2024 13:40 - 14:00 People: Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, Andreas Pavlogiannis
… stronger than all known results:~the problem remains NP-complete even in its \emph …
Implementation and Synthesis of Math Library Functions
POPL When: Wed 17 Jan 2024 10:30 - 10:50 People: Ian Briggs, Yash Lad, Pavel Panchekha
… . This ultimately puts development of such functions out of reach for all but the most …
Monotonicity and the Precision of Program Analysis
POPL When: Fri 19 Jan 2024 11:10 - 11:30 People: Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, Caterina Urban
… . This class includes all non-relational abstract domains that refine interval …
Securing Verified IO Programs Against Unverified Code in F*
POPL When: Fri 19 Jan 2024 16:50 - 17:10 People: Cezar-Constantin Andrici, Stefan Ciobaca, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Theo Winterhalter
… to perform all IO actions via a secure IO library, which uses reference monitoring …
VST-A: A Foundationally Sound Annotation Verifier
POPL When: Fri 19 Jan 2024 15:30 - 15:50 People: Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao
… of the rich assertion language, not all reduced proof goals can be automatically checked …
Orthologic with Axioms
POPL When: Fri 19 Jan 2024 16:50 - 17:10 People: Simon Guilloud, Viktor Kunčak
… that propositional resolution of width 5 proves all formulas provable …
Validation of Modern JSON Schema: Formalization and Complexity
POPL When: Wed 17 Jan 2024 17:30 - 17:50 People: Lyes Attouche, Mohamed-Amine Baazizi, Dario Colazzo, Giorgio Ghelli, Carlo Sartiani, Stefanie Scherzinger
… model. \emph{Modern JSON Schema} is the name used to indicate all versions from …
Disentanglement with Futures, State, and Interaction
POPL When: Thu 18 Jan 2024 15:50 - 16:10 People: Jatin Arora, Stefan K. Muller, Umut A. Acar
… that it can be exploited to improve the performance of parallel functional programs. All …
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL When: Wed 17 Jan 2024 17:50 - 18:10 People: Xueying Qin, Liam O'Connor, Rob van Glabbeek, Peter Hoefner, Ohad Kammar, Michel Steuwer
… . The semantics and calculus are formalised in Isabelle/HOL and all proofs have been …
Inference of Robust Reachability Constraints
POPL When: Fri 19 Jan 2024 14:00 - 14:20 People: Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, Sébastien Bardin
… for all uncontrolled input but a few corner cases. To address this issue, we …