.- Type Systems, Safety, and Verification.
.- Memory Safety: Uniqueness as Separation.
.- Fair Termination for Resource-Aware Active Objects.
.- A Formal Foundation for Equational Reasoning on Probabilistic Programs.
.- Control, Effects, and Decidability.
.- Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers.
.- Expressive Power of One-Shot Control Operators and Coroutines.
.- Positive Sharing and Abstract Machines.
.- Quantum Programming and Logic.
.- IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation.
.- A Quantum-Control Lambda-Calculus with Multiple Measurement Bases.
.- Program Analysis, Specifications, and Decision Procedures.
.- Checking Consistency of Event-driven Traces.
.- Specification Inference modulo Oracles for Database-backed Web Applications.
.- Decision Procedures for A Theory of String Sequences.
.- AI and Compiler Optimisation for Performance.
.- ELTC: An End-to-End Large Language Model-Based Tensor Compilation Optimization Framework.
.- Performance Optimization of HPC Workloads in Cloud Using AI-Driven Algorithms.
