yusuke1997/dblp-id-title huggingface dataset:
An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
Precise static modeling of Ethereum "memory"
Seam: provably safe local edits on graphs
Consistency of a Dependent Calculus of Indistinguishability
A pretty but not greedy printer (functional pearl)
Analytical modeling of cache behavior for affine programs
Pointer life cycle types for lock-free data structures with memory reclamation
Flux: Liquid Types for Rust
A Lineage-Based Referencing DSL for Computer-Aided Design
On the semantic expressiveness of recursive types
PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
An Order-Theoretic Analysis of Universe Polymorphism
Verified tensor-program optimization via high-level scheduling rewrites
Testing and debugging functional reactive programming
A derivation framework for dependent security label inference
Foundations of empirical memory consistency testing
Thriving in a crowded and changing world: C++ 2006-2020
Locally Nameless Sets
IDE al : efficient and precise alias-aware dataflow analysis
Contextual equivalence for a probabilistic language with continuous random variables and recursion
Hashing Modulo Context-Sensitive 𝛼-Equivalence
Keep your laziness in check
Random Variate Generation with Formal Guarantees
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana
Symbolic conditioning of arrays in probabilistic programs
Safer smart contract programming with Scilla
Hadamard-Pi: Equational Quantum Programming
Inferring frame conditions with static correlation analysis
Oracle-free repair synthesis for floating-point programs
An Algebra of Alignment for Relational Verification
Destabilizing Iris
Higher inductive types in cubical computational type theory
Qudit Quantum Programming with Projective Cliffords
Automated Translation of Functional Big Data Queries to SQL
Quantum information effects
Strict and lazy semantics for effects: layering monads and comonads
PlanAlyzer: assessing threats to the validity of online experiments
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
Guided Equality Saturation
Law and Order for Typestate with Borrowing
Data-driven lemma synthesis for interactive proofs
I/O dependent idempotence bugs in intermittent systems
Exceptional asynchronous session types: session types without tiers
Scaling exact inference for discrete probabilistic programs
PyDex: Repairing Bugs in Introductory Python Assignments using LLMs
Exact Loop Bound Analysis
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Fair Operational Semantics
Testing consensus implementations using communication closure
A mechanical formalization of higher-ranked polymorphic type inference
Project snowflake: non-blocking safe manual memory management in .NET
Introduction and elimination, left and right
A spectrum of type soundness and performance
Modular Hardware Design of Pipelined Circuits with Hazards
Verifying correct usage of context-free API protocols
HEaaN.MLIR: An Optimizing Compiler for Fast Ring-Based Homomorphic Encryption
PRIMA: general and precise neural network certification via scalable convex hull approximations
Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
Regular Abstractions for Array Systems
Automated Verification of Fundamental Algebraic Laws
A practical construction for decomposing numerical abstract domains
Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies
Dependency-Aware Compilation for Surface Code Quantum Architectures
ReLU Hull Approximation
Generative type-aware mutation for testing SMT solvers
Effective stateless model checking for C/C++ concurrency
Automatically Reducing Privilege for Access Control Policies
Rich specifications for Ethereum smart contract verification
Semi-symbolic inference for efficient streaming probabilistic programming
A simple soundness proof for dependent object types
Intensional Functions
Iron: managing obligations in higher-order concurrent separation logic
Equality Saturation Theory Exploration à la Carte
Teaching the art of functional programming using automated grading (experience report)
Correctness of speculative optimizations with dynamic deoptimization
Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs
Resolution as intersection subtyping via Modus Ponens
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming
Internalizing Indistinguishability with Dependent Types
JAX Autodiff from a Linear Logic Perspective
SPORE: Combining Symmetry and Partial Order Reduction
On the Expressive Power of String Constraints
Deciding memory safety for single-pass heap-manipulating programs
Seq2Parse: neurosymbolic parse error repair
Staged generic programming
Qubit Recycling Revisited
HiPy: Extracting High-Level Semantics from Python Code for Data Processing
Synbit: synthesizing bidirectional programs using unidirectional sketches
A Core Calculus for Equational Proofs of Cryptographic Protocols
Well-typed programs can go wrong: a study of typing-related bugs in JVM compilers
What happens-after the first race? enhancing the predictive power of happens-before based dynamic race detection
On the unusual effectiveness of type-aware operator mutations for testing SMT solvers
Bringing the WebAssembly Standard up to Speed with SpecTec
V-Star: Learning Visibly Pushdown Grammars from Program Inputs
A Calculus for Amortized Expected Runtimes
Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs
Higher-order probabilistic adversarial computations: categorical semantics and program logics
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8
Generic go to go: dictionary-passing, monomorphisation, and hybrid
LooPy: interactive program synthesis with control structures
A predicate transformer semantics for effects (functional pearl)
Static Analysis of Memory Models for SMT Encodings
Better Defunctionalization through Lambda Set Specialization
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
A type-and-effect system for object initialization
SteelCore: an extensible concurrent separation logic for effectful dependently typed programs
A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis
A formal foundation for symbolic evaluation with merging
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)
Program synthesis with algebraic library specifications
A separation logic for heap space under garbage collection
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Oblivious algebraic data types
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
The (In)Efficiency of interaction
Verus: Verifying Rust Programs using Linear Ghost Types
Interactive Debugging of Datalog Programs
DiffStream: differential output testing for stream processing programs
Rebuilding racket on chez scheme (experience report)
Graduality from embedding-projection pairs
Semantic Logical Relations for Timed Message-Passing Protocols
Effects as capabilities: effect handlers and lightweight effect polymorphism
Sound gradual typing is nominally alive and well
Symbolic execution for randomized programs
Linearly qualified types: generic inference for capabilities and uniqueness
The decidability and complexity of interleaved bidirected Dyck reachability
JavaScript: the first 20 years
Visualization by example
From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing
Solving Floating-Point Constraints with Continuous Optimization
Statically bounded-memory delayed sampling for probabilistic streams
A fine-grained computational interpretation of Girard's intuitionistic proof-nets
Intrinsically typed compilation with nameless labels
Fault tolerant functional reactive programming (functional pearl)
Probabilistic Refinement Session Types
Optimizing Ancilla-Based Quantum Circuits with SPARE
Towards a formal foundation of intermittent computing
Effectful program distancing
Sequential programming for replicated data stores
LWeb: information flow security for multi-tier web applications
The Logical Essence of Well-Bracketed Control Flow
The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
Seq: a high-performance language for bioinformatics
A Verified High-Performance Composable Object Library for Remote Direct Memory Access
FrAngel: component-based synthesis with control structures
Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts
Semantic programming by example with pre-trained models
Foundational Multi-Modal Program Verifiers
Formally verified speculation and deoptimization in a JIT compiler
Compiling Recurrences over Dense and Sparse Arrays
Newly-single and loving it: improving higher-order must-alias analysis with heap fragments
Dependent Coeffects for Local Sensitivity Analysis
Static stages for heterogeneous programming
Seminaïve evaluation for a higher-order functional language
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly
Effect handlers for the masses
Allo: A Programming Model for Composable Accelerator Design
Checking Observational Correctness of Database Systems
Generating a fluent API with syntax checking from an LR grammar
A principled approach to ornamentation in ML
LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Taylor subsumes Scott, Berry, Kahn and Plotkin
Normalization by evaluation for sized dependent types
Gradual Typing for Effect Handlers
Higher-Order Property-Directed Reachability
Safety and conservativity of definitions in HOL and Isabelle/HOL
A domain theory for statistical probabilistic programming
Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Verified code generation for the polyhedral model
A framework for adaptive differential privacy
Verifying strong eventual consistency in distributed systems
From fine- to coarse-grained dynamic information flow control and back
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction
Aeneas: Rust verification by functional translation
Programming at the edge of synchrony
The history of Standard ML
Arbitration-Free Consistency Is Available (and Vice Versa)
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers
The Path to Durable Linearizability
QbC: Quantum Correctness by Construction
Polyadic approximations, fibrations and intersection types
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
A formalization of Java's concurrent access modes
Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities
Efficient Bottom-Up Synthesis for Programs with Local Variables
CPS transformation with affine types for call-by-value implicit polymorphism
Architecture-Preserving Provable Repair of Deep Neural Networks
Soft contract verification for higher-order stateful programs
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization
Constructing quotient inductive-inductive types
Efficient CHAD
Synthesizing coupling proofs of differential privacy
Embedding by Unembedding
A Pretty Expressive Printer
Imperative functional programs that explain their work
Logarithm and program testing
Design and Implementation of an Aspect-Oriented C Programming Language
Efficient Linearizability Monitoring
Theorems for free from separation logic specifications
Divergence-Aware Testing of Graphics Shader Compiler Back-Ends
Guided Tensor Lifting
Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
Verification of Bit-Flip Attacks against Quantized Neural Networks
Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
Theorems for free for free: parametricity, with and without types
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
Structural versus pipeline composition of higher-order functions (experience report)
Domain-Theoretic Semantics for Functional Logic Programming
Go with the flow: compositional abstractions for concurrent data structures
Casting about in the dark: an empirical study of cast operations in Java programs
MLstruct: principal type inference in a Boolean algebra of structural types
Adaptive Shielding via Parametric Safety Proofs
Distributed causal memory: modular specification and verification in higher-order distributed separation logic
Sparcl: a language for partially-invertible computation
Historia: Refuting Callback Reachability with Message-History Logics
Inductive Diagrams for Causal Reasoning
Fulminate: Testing CN Separation-Logic Specifications in C
Bayesian synthesis of probabilistic programs for automatic data modeling
Deductive optimization of relational data storage
Compositional embeddings of domain-specific languages
An Incremental Algorithm for Algebraic Program Analysis
Automated Verification of Parametric Channel-Based Process Communication
Efficient, Portable, Census-Polymorphic Choreographic Programming
A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
Counting and Sampling Traces in Regular Languages
Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs
Formal reasoning about layered monadic interpreters
Sensitivity by Parametricity
Semantics Lifting for Syntactic Sugar
CoolerSpace: A Language for Physically Correct and Computationally Efficient Color Programming
Equivalence and Similarity Refutation for Probabilistic Programs
Indexing the extended Dyck-CFL reachability for context-sensitive program analysis
Reward Augmentation in Reinforcement Learning for Testing Distributed Systems
Hardware-Aware Static Optimization of Hyperdimensional Computations
Interactive synthesis of temporal specifications from examples and natural language
Duplo: a framework for OCaml post-link optimisation
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Programming and reasoning with partial observability
DeepSEA: a language for certified system software
Better late than never: a fully-abstract semantics for classical processes
Circuit Optimization using Arithmetic Table Lookups
Kami: a platform for high-level parametric hardware specification and its modular verification
Recursive Program Synthesis using Paramorphisms
Programmable MCMC with Soundly Composed Guide Programs
A²I: abstract² interpretation
What's decidable about linear loops?
Raising expectations: automating expected cost analysis with types
Weighted Context-Free-Language Ordered Binary Decision Diagrams
Towards verified stochastic variational inference for probabilistic programs
A general approach to define binders using matching logic
Verified Density Compilation for a Probabilistic Programming Language
Randomized Testing of Byzantine Fault Tolerant Algorithms
Grounded Copilot: How Programmers Interact with Code-Generating Models
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks
Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)
Jmvx: Fast Multi-threaded Multi-version Execution and Record-Replay for Managed Languages
Decision and Complexity of Dolev-Yao Hyperproperties
Optimal Dyck reachability for data-dependence and alias analysis
Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
Taming type annotations in gradual typing
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
Promises are made to be broken: migrating R to strict semantics
Speeding up symbolic reasoning for relational queries
Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network
Abstract Interpreters: A Monadic Approach to Modular Verification
Koord: a language for programming and verifying distributed robotics application
The taming of the rew: a type theory with computational assumptions
Reducing liveness to safety in first-order logic
Cosmo: a concurrent separation logic for multicore OCaml
Don't Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation
Interpretable noninterference measurement and its application to processor designs
A reasonably exceptional type theory
Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores
MemPerf: Profiling Allocator-Induced Performance Slowdowns
Compound Memory Models
Featherweight go
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems
Recovering purity with comonads and capabilities
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
Identifying refactoring opportunities for replacing type code with subclass and state
Static detection of silent misconfigurations with deep interaction analysis
Trace-Guided Inductive Synthesis of Recursive Functional Programs
StacKAT: Infinite State Network Verification
Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
Less is more: multiparty session types revisited
Bit Blasting Probabilistic Programs
Multi types and reasonable space
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Visibility reasoning for concurrent snapshot algorithms
Generating precise error specifications for C: a zero shot learning approach
Determination Problems for Orbit Closures and Matrix Groups
Predictive Monitoring against Pattern Regular Languages
Strategy synthesis for linear arithmetic games
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
Type-Safe Dynamic Placement with First-Class Placed Values
The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
Deterministic parallel fixpoint computation
Dynamic Region Ownership for Concurrency Safety
Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself
Revisiting iso-recursive subtyping
Intersection types and (positive) almost-sure termination
A relational logic for higher-order programs
Precision-preserving yet fast object-sensitive pointer analysis with partial context sensitivity
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS
Quotient Haskell: Lightweight Quotient Types for All
How to Bake a Quantum Π
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
Conditional Contextual Refinement
Translating canonical SQL to imperative code in Coq
Connectivity graphs: a method for proving deadlock freedom based on separation logic
Constraint-based type inference for FreezeML
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats
Formal Specification and Testing for Reinforcement Learning
Verilog HDL and its ancestors and descendants
Consistent Updates for Scalable Microservices
Mostly Automated Proof Repair for Verified Libraries
ιDOT: a DOT calculus with object initialization
A probabilistic separation logic
Exposing cache timing side-channel leaks through out-of-order symbolic execution
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
QuickSilver: modeling and parameterized verification for distributed agreement-based systems
Program synthesis using abstraction refinement
Optimization of swift protocols
Functional collection programming with semi-ring dictionaries
Sound Dynamic Deadlock Prediction in Linear Time
On polymorphic gradual typing
Polymorphic Records for Dynamic Languages
Horn-ICE learning for synthesizing invariants and contracts
Parallelization of dynamic languages: synchronizing built-in collections
Relational nullable types with Boolean unification
StreamQL: a query language for processing streaming time series
Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
TLC: temporal logic of distributed components
SecRSL: security separation logic for C11 release-acquire concurrency
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
Staged abstract interpreters: fast and modular whole-program analysis via meta-programming
A Typed Multi-level Datalog IR and Its Compiler Framework
FlashProfile: a framework for synthesizing data profiles
Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation
Closure conversion is safe for space
Cryptis: Cryptographic Reasoning in Separation Logic
A systematic approach to deriving incremental type checkers
Applying cognitive principles to model-finding output: the positive value of negative information
Compiling with continuations, correctly
The Essence of Generalized Algebraic Data Types
Trace abstraction modulo probability
Adequacy for Algebraic Effects Revisited
Accelerating Fuzzing through Prefix-Guided Execution
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
Trustworthy Runtime Verification via Bisimulation (Experience Report)
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
Abstracting gradual typing moving forward: precise and space-efficient
Cubical agda: a dependently typed programming language with univalence and higher inductive types
Coq Coq correct! verification of type checking and erasure for Coq, in Coq
KestRel: Relational Verification using E-Graphs for Program Alignment
An Iris Instance for Verifying CompCert C Programs
Compilation of Modular and General Sparse Workspaces
Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam
Polynomial Time and Dependent Types
A specification for dependent types in Haskell
Structuring the synthesis of heap-manipulating programs
Context-bounded verification of thread pools
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
Actor concurrency bugs: a comprehensive study on symptoms, root causes, API usages, and differences
egg: Fast and extensible equality saturation
Hyperfunctions: Communicating Continuations
Exploiting implicit beliefs to resolve sparse usage problem in usage-based specification mining
Compositionality and Observational Refinement for Linearizability with Crashes
Verifying distributed programs via canonical sequentialization
Scalable and serializable networked multi-actor programming
Lightweight and Locality-Aware Composition of Black-Box Subroutines
A sparse iteration space transformation framework for sparse tensor algebra
Efficient Matching of Regular Expressions with Lookaround Assertions
Probabilistic Kleene Algebra with Angelic Nondeterminism