Search events for 'all'
Recursive Subtyping for All
POPL When: Wed 18 Jan 2023 11:35 - 12:00 People: Litao Zhou, Yaoda Zhou, Bruno C. d. S. Oliveira
… to the conventional (upper) bounded quantification of $F_\le$. All the results …
From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
PADL 2023 When: Tue 17 Jan 2023 14:30 - 15:00 People: Misaki Kojima, Naoki Nishida
… An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically … represented by a logically constrained term rewrite system to an all-path reachability …
Imagining the Reader
PLMW @ POPL 2023 When: Tue 17 Jan 2023 09:15 - 10:00 People: Benjamin C. Pierce
… Writing well on technical subjects is hard for many reasons, but perhaps the hardest of all is the difficulty of imagining what it is like not to know something that we do know. We’ll explore some approaches to this challenge. …
Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation
CoqPL 2023 When: Sat 21 Jan 2023 11:00 - 11:30 People: Dustin Jamner, Gabriel Kammer, Adam Chlipala
… all other cases. This is made possible by an inductive formulation …, so all compiler-correctness proofs boil down to type-checking and equational …
Towards a Reflection for Effect Handlers
PEPM 2023 When: Tue 17 Jan 2023 16:30 - 17:00 People: Youyou Cong, Kenichi Asai
… as the compiling function, we can prove most but not all theorems required of a reflection …
Omnisemantics: Smooth Handling of Nondeterminism (Invited talk)
CoqPL 2023 When: Sat 21 Jan 2023 09:00 - 10:00 People: Samuel Gruetter
… starting state and program describes all possible nondeterministic executions (hence … compiled to nondeterministic target languages.
All results have been formalized …
Symbolic Execution of Hadamard-Toffoli Quantum Circuits
PEPM 2023 When: Tue 17 Jan 2023 11:30 - 12:00 People: Jacques Carette, Gerardo Ortiz, Amr Sabry
… generated over the symbolic variables contains all the necessary quantum …
FaJITa: Verifying Optimizations on Just-In-Time Programs
PriSC 2023 When: Sat 21 Jan 2023 16:25 - 16:50 People: David Thien, Michael Smith, Evan Johnson, Sorin Lerner, Hovav Shacham, Deian Stefan, Fraser Brown
… Firefox’s optimizing JIT compiler. We are able to verify practically all …
Fast Cryptographic Code via Partial Evaluation
PEPM 2023 When: Tue 17 Jan 2023 09:00 - 10:00 People: Adam Chlipala
… This presentation is an overview of and update on our project Fiat Cryptography, which uses the Coq proof assistant to generate fast cryptographic code, with proof of correctness. Code produced with this tool is now included by all major …
Designing an experiment for comparing user interfaces for legal formalization
ProLaLa 2023 When: Sun 15 Jan 2023 16:45 - 17:10 People: Tereza Novotná, Tomer Libal
… in order to create such knowledge bases. A major goal of all the approaches …
The Structure and Legal Interpretation of Computer Programs
ProLaLa 2023 When: Sun 15 Jan 2023 11:50 - 12:15 People: James Grimmelmann
… , it is conventional all the same. …
Exact Inference for Discrete Probabilistic Programs via Generating Functions
LAFI 2023 When: Sun 15 Jan 2023 10:10 - 10:20 People: Fabian Zaiser, C.-H. Luke Ong
… nested inference. All of this is possible because we work with \emph{probability …
Differential Verification of Deep Neural Networks
VMCAI 2023 When: Tue 17 Jan 2023 09:00 - 10:00 People: Chao Wang
… bound their maximum difference over all inputs. We also propose automated …
Distributing and Parallelizing Non-canonical Loops
VMCAI 2023 When: Mon 16 Jan 2023 10:00 - 10:30 People: Clément Aubert, Thomas Rubiano, Neea Rusch, Thomas Seiller
… , language-agnostic, proven correct, and applicable to all types of loops …
What Can Program Analysis Say About Data Bias?
VMCAI 2023 When: Mon 16 Jan 2023 14:00 - 15:00 People: Aws Albarghouthi
… infinite, number of datasets, ensuring that they all produce the same prediction …
Building Information Modeling Using Constraint Logic Programming (Extended Abstract)
ProLaLa 2023 When: Sun 15 Jan 2023 11:00 - 11:25 People: Joaquín Arias, Seppo Törmä, Manuel Carro, Gopal Gupta
… city), if at all possible. This paper is an extended abstract of Arias et al …
Towards a Theoretical Understanding of Property-Directed Reachability
VMCAI 2023 When: Mon 16 Jan 2023 09:00 - 10:00 People: Sharon Shoham
… version of PDR, called Lambda-PDR, in which all generalizations …
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
CPP 2023 When: Mon 16 Jan 2023 11:00 - 11:22 People: Christina Kohl, Aart Middeldorp
… eluded all formalization attempts. We present a formalization in the proof …
Introduction to the tensor-programs framework, a PL approach that helps analyse theoretical properties of deep learning.
LAFI 2023 When: Sun 15 Jan 2023 09:05 - 10:05 People: Hongseok Yang
… computations of networks of nearly all architectures.The most important part … network architectures to nearly all architectures.
The goal of my talk …
Modern Macros
PADL 2023 When: Tue 17 Jan 2023 09:00 - 10:00 People: Robert Bruce Findler
… an intellectual foundation for understanding modern macros. These aspects all center …
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
CPP 2023 When: Tue 17 Jan 2023 17:07 - 17:30 People: Anne Baanen, Alex Best, Nirvana Coppola, Sander R. Dahmen
… Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form $y^2=x^3+d$, where $d$ is a (given) nonzero integer number and all solutions in integers …
Practical and sound equality tests, automatically
CPP 2023 When: Tue 17 Jan 2023 11:45 - 12:07 People: Benjamin Gregoire, Jean-Christophe Léchenet, Enrico Tassi
… no existing tool has all the features above, which are used in real Coq … benchmark it, showing that thanks to its better complexity it outperforms all …
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
CPP 2023 When: Mon 16 Jan 2023 12:07 - 12:30 People: Yannick Forster, Felix Jahn, Gert Smolka
… ''. All proofs are machine-checked in Coq but should transport to other foundations …
Statically Resolvable Ambiguity
POPL When: Thu 19 Jan 2023 14:20 - 14:45 People: Viktor Palmkvist, Elias Castegren, Philipp Haller, David Broman
… of resolving the ambiguity to the end user. If all programs accepted by an ambiguous …—for all programs—is hard, where previous work only solves it partially using …
Conditional Contextual Refinement
POPL When: Wed 18 Jan 2023 14:20 - 14:45 People: Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer
… . A number of verification frameworks employ these techniques in tandem, but in all … into a unified mechanism enjoying all the benefits of refinement and separation …
Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
POPL When: Fri 20 Jan 2023 09:25 - 09:50 People: Han Xu, Xuejing Huang, Bruno C. d. S. Oliveira
… operator. We
have implemented type difference and all the operators % presented in this paper
in the CP language. Moreover, all the calculi and related proofs …
Isabelle/HOL: Foundations, Induction, and Coinduction
TutorialFest When: Mon 16 Jan 2023 09:00 - 10:30Mon 16 Jan 2023 11:00 - 12:30 People: Andrei Popescu, Dmitriy Traytel
… we will continue to use Isabelle for all our hands-on examples and exercises …
Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
POPL When: Fri 20 Jan 2023 15:35 - 16:00 People: Yuanbo Li, Qirun Zhang, Thomas Reps
… variant, it is feasible to summarize all paths from the source node to the target … of algorithms: (1) the general all-pairs InterDyck-reachability algorithms based … benchmarks compared to all-pair LCL-reachability, SPDS-reachability, and domain …
Towards a Higher-Order Mathematical Operational Semantics
POPL When: Fri 20 Jan 2023 17:35 - 18:00 People: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat
… compositionality result that applies to all systems specified in this way and discuss …
Grisette: Symbolic Compilation as a Functional Programming Library
POPL When: Fri 20 Jan 2023 17:10 - 17:35 People: Sirui Lu, Rastislav Bodík
… -specific symbolic compilers. Grisette evaluates all execution paths and merges …
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
POPL When: Fri 20 Jan 2023 10:45 - 11:10 People: Alejandro Aguirre, Lars Birkedal
… with the maximal and minimal probabilities of
termination under all schedulers. Finally …
Witnessability of Undecidable Problems
POPL When: Wed 18 Jan 2023 13:30 - 13:55 People: Shuo Ding, Qirun Zhang
… surprising fact is that the class of witnessable problems includes almost all …. In particular, all ``non-trivial semantic properties of programs'' mentioned …
A Core Calculus for Equational Proofs of Cryptographic Protocols
POPL When: Wed 18 Jan 2023 16:00 - 16:25 People: Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, Greg Morrisett
… . All proofs of case studies are mechanized via an embedding of IPDL into the Coq …
Why Are Proofs Relevant in Proof-Relevant Models?
POPL When: Fri 20 Jan 2023 17:10 - 17:35 People: Axel Kerinec, Giulio Manzonetto, Federico Olimpieri
… that they can be presented as type systems as well.
We prove that all the models …
Locally Nameless Sets
POPL When: Fri 20 Jan 2023 16:45 - 17:10 People: Andrew M. Pitts
… in the literature to model variable renaming operations on syntax with binders are all …
A Formalization of Observational Equivalence in Message Passing Protocols
Student Research Competition When: Wed 18 Jan 2023 18:00 - 19:30 People: Nathan Liittschwager
… , with the implicit understanding that all protocols are “equivalent” with respect …
A High-Level Separation Logic for Heap Space under Garbage Collection
POPL When: Wed 18 Jan 2023 13:30 - 13:55 People: Alexandre Moine, Arthur Charguéraud, François Pottier
… . All of our results are proved in
Coq on top of Iris. …
A Partial Order View of Message-Passing Communication Models
POPL When: Wed 18 Jan 2023 11:35 - 12:00 People: Cinzia Di Giusto, Davide Ferre', Laetitia Laversa, Etienne Lozes
… , based on their concurrent behaviors. We also show that all the communication models …
Unrealizability Logic
POPL When: Wed 18 Jan 2023 16:00 - 16:25 People: Jinwoo Kim, Loris D'Antoni, Thomas Reps
…
to establish that a problem is unrealizable;
however, these techniques are all …
The Fine-Grained Complexity of CFL Reachability
POPL When: Fri 20 Jan 2023 15:10 - 15:35 People: Paraschos Koutris, Shaleen Deep
… to all algorithms, and shows that CFL reachability is strictly harder that Boolean …
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
POPL When: Fri 20 Jan 2023 09:00 - 09:25 People: Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, Steve Zdancewic
… that demonstrates how unions,
intersections, and overloading can all coexist …
Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
POPL When: Wed 18 Jan 2023 17:35 - 18:00 People: Wonyeol Lee, Xavier Rival, Hongseok Yang
… accurately, and making our improved pathwise gradient estimator exploit all …
Tail Recursion Modulo Context: An Equational Approach
POPL When: Fri 20 Jan 2023 13:30 - 13:55 People: Daan Leijen, Anton Lorenzen
… reason about the soundness of in-place update. While all previous
approaches …
Context-Bounded Verification of Context-Free Specifications
POPL When: Fri 20 Jan 2023 16:00 - 16:25 People: Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
… ask that all behaviors generated in runs of bounded number of context switches …
Using a Proof Assistant to Teach PL Theory, Without the Overhead
TutorialFest When: Mon 16 Jan 2023 14:00 - 15:30Mon 16 Jan 2023 16:00 - 17:30 People: Jonathan Aldrich, John Boyland
… with these assignments, all used at CMU and suitable for incorporation in other PL …