IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation

This chapter introduces a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL) extended with a modality that captures the transition from pure to mixed states in quantum computation. The research defines the logic -IMALL by extending IMALL with a modality in a transparent way, supporting both pure and mixed-state computation within a unified logical setting. The proof language offers three major advantages over typical quantum lambda calculi: it enables a richer linear-algebraic structure, allows the expression of genuinely quantum control flows, and dispenses with the need for an external global configuration. The chapter also presents a denotational model inspired by previous work, validating the design of the language and supporting an adequacy theorem. Additionally, the expressive power of the language is demonstrated through examples such as quantum teleportation and the quantum switch, highlighting its ability to naturally capture paradigmatic quantum phenomena. The structure of the paper includes sections on syntax, derivation rules, cut-elimination, categorical model, denotational semantics, and encoding quantum computing, providing a comprehensive overview of the novel proof language and its applications in quantum computation.