Quantum Programming / Domain-Specific Languages.- Circuit Width Estimation via Effect Typing and Linear Dependency.- On the Hardness of Analyzing Quantum Programs Quantitatively.- Reconciling Partial and Local Invertibility.- Efficient Matching with Memorization for Regexes with Look-around and Atomic Grouping.- Verification.- A Denotational Approach to Release/Acquire Concurrency.- Intel PMDK Transactions: Specification, Validation and Concurrency.
- Artifact report: Intel PMDK Transactions: Specification, Validation and Concurrency.- Verifying Persistent Libraries.- Hyperproperty Verification as CHC Satisfiability.- Program Analysis.- Maximal Quantified Precondition Synthesis for Linear Array Loops.- Verified Inlining and Specialisation for PureCake.- Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages.- Higher-Order LCTRSs and Their Termination.
- Abstract Interpretation A Modular Soundness Theory for the Blackboard Analysis Architecture.- Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation.- Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law .