Events (45 results)

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 …

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 …

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 …

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

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 …

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 …

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 …

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

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 …

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 …

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

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 …

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 …

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 …

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 …

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 …

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 …

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

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

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 …

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 …

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

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 …

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 …

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 …

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 …

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

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 …

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 …