A new connective in natural deduction, and its application to quantum computing

DOI10.1016/j.tcs.2023.113840OpenAlexW3196572487MaRDI QIDQ5925711

Gilles Dowek, Alejandro Díaz-Caro

Publication date: 27 April 2023

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2023.113840

zbMATH Keywords

quantum computinglambda calculustype theoryproof-reduction

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• General-elimination stability
• General-elimination harmony and the meaning of the logical constants
• Higher-order rewrite systems and their confluence
• Combinatory reduction systems: Introduction and survey
• Natural deduction with general elimination rules
• A formal framework for specifying sequent calculus proof systems
• The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony
• Picturing Quantum Processes
• On quantum lambda calculi: a foundational perspective
• The algebraic lambda calculus
• A natural extension of natural deduction
• Identity and harmony
• Semantics for first-order superposition logic
• A proof theory for generic judgments
• Propositional superposition logic
• A lambda calculus for quantum computation with classical control