Double-Ended Bit-Stealing for Algebraic Data Types

2024-8-15

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

2024-8-15

Functional Programming in Financial Markets (Experience Report)

2024-8-15

Call-by-Unboxed-Value

2024-8-15

Closure-Free Functional Programming in a Two-Level Type Theory

2024-8-15

Almost-Sure Termination by Guarded Refinement

2024-8-15

A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler

2024-8-15

Snapshottable Stores

2024-8-15

A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction

2024-8-15

Dependent Ghosts Have a Reflection for Free

2024-8-15

Refinement Composition Logic

2024-8-15

On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs

2024-8-15

Sound Borrow-Checking for Rust via Symbolic Semantics

2024-8-15

Abstracting Effect Systems for Algebraic Effect Handlers

2024-8-15

Contextual Typing

2024-8-15

Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis

2024-8-15

A Coq Mechanization of JavaScript Regular Expression Semantics

2024-8-15

Parallel Algebraic Effect Handlers

2024-8-15

Gradual Indexed Inductive Types

2024-8-15

The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl)

2024-8-15

The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures

2024-8-15

Compiled, Extensible, Multi-language DSLs (Functional Pearl)

2024-8-15

Abstract Interpreters: A Monadic Approach to Modular Verification

2024-8-15

Specification and Verification for Unrestricted Algebraic Effects and Handling

2024-8-15

How to Bake a Quantum Π

2024-8-15

Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs

2024-8-15

Example-Based Reasoning about the Realizability of Polymorphic Programs

2024-8-15

Oxidizing OCaml with Modal Memory Management

2024-8-15

Staged Compilation with Module Functors

2024-8-15

Grokking the Sequent Calculus (Functional Pearl)

2024-8-15

CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs

2024-8-15

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System

2024-8-15

Synchronous Programming with Refinement Types

2024-8-15

Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts

2024-8-15

Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)

2024-8-15

V-Star: Learning Visibly Pushdown Grammars from Program Inputs

2024-6-20

GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables

2024-6-20

Mechanised Hypersafety Proofs about Structured Data

2024-6-20

Verified Extraction from Coq to OCaml

2024-6-20

Jacdac: Service-Based Prototyping of Embedded Systems

2024-6-20

Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs

2024-6-20

From Batch to Stream: Automatic Generation of Online Algorithms

2024-6-20

Allo: A Programming Model for Composable Accelerator Design

2024-6-20

Symbolic Execution for Quantum Error Correction Programs

2024-6-20

VESTA: Power Modeling with Language Runtime Events

2024-6-20

Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments

2024-6-20

A Verified Compiler for a Functional Tensor Language

2024-6-20

RefinedRust: A Type System for High-Assurance Verification of Rust Programs

2024-6-20

Descend: A Safe GPU Systems Programming Language

2024-6-20

Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq

2024-6-20