Binding Structures as an Abstract Data Type
Abstract elided by the publisher.
976 papers · page 18 of 49
Full Reduction in the Face of Absurdity
Abstract elided by the publisher.
Type Targeted Testing
We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be viewed as a high-level, declarative, test g…
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
We present a lightweight approach to Hoare-style specifications for fine-grained concurrency, based on a notion of time-stamped histories that abstractly capture atomic changes in the program state. Our key observation is that histories form a partial commutative monoid, a struct…
A Separation Logic for Fictional Sequential Consistency
Abstract elided by the publisher.
Monotonic References for Efficient Gradual Typing
Abstract elided by the publisher.
Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
Abstract elided by the publisher.
Running Probabilistic Programs Backwards
Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification—except that all such probabilistic…
Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages
Abstract elided by the publisher.
Grounding Synchronous Deterministic Concurrency in Sequential Programming
Abstract elided by the publisher.
A Coq Formalization of the Relational Data Model
Abstract elided by the publisher.
Verified Compilation for Shared-Memory C
Abstract elided by the publisher.
Resolving Non-determinism in Choreographies
Abstract elided by the publisher.
Model and Proof Generation for Heap-Manipulating Programs
Abstract elided by the publisher.
A Core Quantitative Coeffect Calculus
Abstract elided by the publisher.
Overlapping and Order-Independent Patterns - Definitional Equality for All
Abstract elided by the publisher.
On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi
Probabilistic applicative bisimulation is a recently introduced coinductive methodology for program equivalence in a probabilistic, higher-order, setting. In this paper, the technique is applied to a typed, call-by-value, lambda-calculus. Surprisingly, the obtained relation coinc…
The Duality of Construction
Abstract elided by the publisher.
Staged Composition Synthesis
Abstract elided by the publisher.
Targeted Update - Aggressive Memory Abstraction Beyond Common Sense and Its Application on Static Numeric Analysis
Abstract elided by the publisher.