613 papers · page 1 of 31
Positive Sharing and Abstract Machines
A Formal Foundation for Equational Reasoning on Probabilistic Programs
Memory Safety: Uniqueness as Separation
Fair Termination for Resource-Aware Active Objects
IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality B to capture mixed-state quantum computation. The language supports algebraic constructs such as linear combinations, and embeds pure quantum computations withi…
A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements. We formalise its…
Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers
Decision Procedure for a Theory of String Sequences
Performance Optimization of HPC Workloads in Cloud Using AI-Driven Algorithms
Expressive Power of One-Shot Control Operators and Coroutines
ELTC: An End-to-End Large Language Model-Based Tensor Compilation Optimization Framework
Specification Inference Modulo Oracles for Database-Backed Web Applications
Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories
Algebraic theories with dependency between sorts form the structural core of Martin-L\"of type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (co…
Extending the Quantitative Pattern-Matching Paradigm
Quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers
A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution
Non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures
Hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions
Quantum Programming Without the Quantum Physics
Abstract We propose a quantum programming paradigm where all data are familiar classical data, and the only non-classical element is a random number generator that can return results with negative probability. Currently, the vast majority of quantum programming languages instead …