archive
Every paper Pith has read. Search by title, abstract, or pith.
185 papers in cs.PL · page 1
-
Parameterized program safety reduces to local proofs
Complete Local Reasoning About Parameterized Programs Over Topologies
-
Soundness of natural reductions is coNP-hard even with locks
On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
-
Amaryllis adds dynamic allocation to probabilistic logics
First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
-
Bitstring propagation optimizes T gates in linear time
Linear-Time T-Gate Optimization via Random Abstraction
-
Subtyping merges equivalent paths in tree automata for faster synthesis
Liquid Tree Automata
-
Lattice structures LLM judgments for reliable program analysis
Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis
-
MinTEJ terminal editor for Julia uses less memory than VS Code
Minimalistic Terminal Editor for Julia Programming -- MinTEJ: A Friendly Approach for a Scientific Programmer
-
Categorical triple formalizes LLM agent harness design
Harness Engineering as Categorical Architecture
-
Diversified replicas detect correlated faults by ignoring addresses
Divergent Multi-Version Execution (DME): Canonical Instruction-Trace Fault Detection via Structural Address-Space Decorrelation
-
Generic type system automates heap cost analysis
Automated Amortised Analysis of Skew Heaps and Leftist Heaps (Extended Version)
-
Guided LLMs translate APL legacy code to working C#
Neural Code Translation of Legacy Code: APL to C#
-
OverrideFuzz reaches script boundary behaviors via override modeling
OverrideFuzz: Semantic-Aware Grammar Fuzzing for Script-Runtime Vulnerabilities
-
Symbolic analysis quantifies fraction of inputs changed by patches
Quantitative Symbolic Patch Impact Analysis
-
Git-like trace lets meta-agents fork past states 5x faster than Docker
Shepherd: A Runtime Substrate Empowering Meta-Agents with a Formalized Execution Trace
-
Bounded-preemption SC verification easy only for single writers
Verifying Sequential Consistency under Bounded Preemptions
-
Move prover checks first-class functions with state changes
Formal Verification of Imperative First-Class Functions in Move
-
Move Prover verifies first-class imperative functions
Formal Verification of Imperative First-Class Functions in Move
-
Tool pairs weakest-precondition analysis with AI to infer Move specs
Combining Mechanical and Agentic Specification Inference for Move
-
Hybrid analysis and AI infers Move specifications
Combining Mechanical and Agentic Specification Inference for Move
-
LLM smart contracts score 8.29 points above human versions
SmartEval: A Benchmark for Evaluating LLM-Generated Smart Contracts from Natural Language Specifications
-
CaMPL type system blocks deadlocks in concurrent code
Categorical Message Passing Language (CaMPL) for programmers
-
Credits on thunks make amortised analysis sound for persistent structures
Persistent Amortised Analysis, Operationally
-
Verification takes ten times more effort than credible compilation
Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
-
Benchmark reveals CUDA LLM fixers often degenerate code for tests
CUDABeaver: Benchmarking LLM-Based Automated CUDA Debugging
-
Elevator statically translates entire x86-64 binaries to AArch64
Deterministic Fully-Static Whole-Binary Translation without Heuristics
-
Elevator statically translates entire x86-64 binaries to AArch64 by generating separate…
Deterministic Fully-Static Whole-Binary Translation without Heuristics
-
Refinement types act as ordinary types in Scala 3
First-Class Refinement Types for Scala
-
Lean types catch hardware defects that syntax misses
CktFormalizer: Autoformalization of Natural Language into Circuit Representations
-
Lean 4 type system turns LLM circuits into 95-100% backend successes
CktFormalizer: Autoformalization of Natural Language into Circuit Representations
-
Lean types turn LLM hardware designs into fully realizable circuits
CktFormalizer: Autoformalization of Natural Language into Circuit Representations
-
Proof states become inspectable at source code level
A New Interaction Concept for Interactive and Autoactive Program Verification
-
Controlled unsoundness yields sound bounds for non-monotone fixed points
Bounding Fixed Points of Non-Monotone Processes: Theory to Practice
-
14B model translates GIMPLE to LLVM IR better than 1000B models
LLM Translation of Compiler Intermediate Representation
-
Symbolic traces train 8B model to beat 32B on code violation detection
Teaching LLMs Program Semantics via Symbolic Execution Traces
-
Cache-free GPU enumeration outperforms priors on MBA synthesis
GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching
-
Execution tests reveal BLEU fails to predict code translation correctness
Beyond BLEU: A Semantic Evaluation Method for Code Translation
-
RISC-V semantics in Rocq links compilers to hardware
Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification
-
Refinement types verify hybrid synchronous programs
Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
-
Probabilistic floating-point error bounds computed far faster
Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
-
Reclassifying eval as a governed effect for AI code synthesis
Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect
-
Eval reclassified as governed effect for runtime code synthesis
Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect
-
Pact maps choreographic protocols to formal games
Pact: A Choreographic Language for Agentic Ecosystems
-
Neural CPS verified in any chosen theorem prover
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
-
Java streams fused at compile time via single mapMulti call
Compile-Time Java Stream Fusion via mapMulti
-
Static checker catches JDBC type errors before runtime
Static Type Checking for Database Access Code
-
One relation characterises must-preorder in all sync and async settings
A uniform characterisation of the (a)synchronous must-preorder
-
Four-step loop produces reliable research benchmarks
How to benchmark: the Measure-Explain-Test-Improve loop
-
Datalog DSL in Lean translates queries to provable theorems
A Shallow Embedding of Datalog in Lean
-
Hoare logic derivations can define interpreters
Towards Definitional Interpreters for Hoare Logics
-
AI-generated Lean proofs certify Axon compiler output without audits
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code