nLab Gilles Barthe

• personal page

Selected writings

On type equivalence:

• Gilles Barthe, Olivier Pons, Type Isomorphisms and Proof Reuse in Dependent Type Theory, in Foundations of Software Science and Computation Structures. FoSSaCS 2001, Lecture Notes in Computer Science 2030, Springer (2001) [doi:10.1007/3-540-45315-6_4]

On setoids in type theory:

• Gilles Barthe, Venanzio Capretta, Olivier Pons, Setoids in type theory, Journal of Functional Programming 13 2 (2003) 261-293 [doi:10.1017/S0956796802004501]

Introducing the quantum programming language CoqQ:

• Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying, CoqQ: Foundational Verification of Quantum Programs [arXiv:2207.11350]

  (in Coq)

Understanding the linear logic-sector of bunched logic as a kind of quantum logic:

• Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, A Quantum Interpretation of Bunched Logic for Quantum Separation Logic, LICS ‘21: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science 75 (2021) 1–14 [arXiv:2102.00329, doi:10.1109/LICS52264.2021.9470673]

category: people