Non-linear Pattern Matching with Backtracking for Non-free Data Types
Abstract elided by the publisher.
26,098 papers · page 408 of 1,305
Automated Synthesis of Functional Programs with Auxiliary Functions
Abstract elided by the publisher.
Shallow Effect Handlers
Abstract elided by the publisher.
New Approaches for Almost-Sure Termination of Probabilistic Programs
We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for the almost-sure termination problem. Moreover, using this approach we can obtain explici…
Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General
Abstract elided by the publisher.
Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine
We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closure…
A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints
Abstract elided by the publisher.
Complexity Analysis of Tree Share Structure
The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a lack of a systematic theoretical study. We show that the first-order theo…
Model Checking Differentially Private Properties
Abstract elided by the publisher.
Particle-Style Geometry of Interaction as a Module System
Abstract elided by the publisher.
Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
Abstract elided by the publisher.
On the Soundness of Call Graph Construction in the Presence of Dynamic Language Features - A Benchmark and Tool Evaluation
Abstract elided by the publisher.
Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models
Abstract elided by the publisher.
Certifying CPS Transformation of Let-Polymorphic Calculus Using PHOAS
Abstract elided by the publisher.
Modular Verification of SPARCv8 Code
Abstract elided by the publisher.
Counterexample Guided Inductive Synthesis Modulo Theories
Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. We propose a new approach to program synthe…
What's Hard About Boolean Functional Synthesis?
Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the specification is met. In this paper, we first show that unless some hard conjectures in complexity …
Constraint-Based Synthesis of Coupling Proofs
Proof by coupling is a classical technique for proving properties about pairs of randomized algorithms by carefully relating (or coupling) two probabilistic executions. In this paper, we show how to automatically construct such proofs for probabilistic programs. First, we present…
Constrained Dynamic Partial Order Reduction
The cornerstone of dynamic partial order reduction (DPOR) is the notion of independence that is used to decide whether each pair of concurrent events p and t are in a race and thus both $$p \cdot t$$ and $$t \cdot p$$ must be explored. We present constrained dynamic partial order…
The Learnability of Symbolic Automata
Symbolic automata (s-FAs) allow transitions to carry predicates over rich alphabet theories, such as linear arithmetic, and therefore extend classic automata to operate over infinite alphabets, such as the set of rational numbers. In this paper, we study the problem of the learna…