Skip to Main content Skip to Navigation
Conference papers

Towards a Curry-Howard Correspondence for Linear, Reversible Computation

Abstract : In this paper, we present a linear and reversible language with inductive and coinductive types, together with a Curry-Howard correspondence with the positive fragment of the logic µMALL: linear logic extended with least fixed points allowing inductive statements. Linear, reversible computation makes an important sub-class of quantum computation without measurement. In the latter, the notion of purely quantum recursive type is not yet well understood. Moreover, models for reasoning about quantum algorithms only provide complex types for classical datatypes: there are usually no types for purely quantum objects beside tensors of quantum bits. This work is a first step towards understanding purely quantum recursive types.
Document type :
Conference papers
Complete list of metadata

https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271484
Contributor : Isabelle Gouat Connect in order to contact the contributor
Submitted on : Friday, June 25, 2021 - 6:10:00 PM
Last modification on : Tuesday, September 28, 2021 - 5:16:00 PM
Long-term archiving on: : Sunday, September 26, 2021 - 10:33:32 PM

Licence


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License

Identifiers

  • HAL Id : lirmm-03271484, version 1

Citation

Kostia Chardonnet, Alexis Saurin, Benoît Valiron. Towards a Curry-Howard Correspondence for Linear, Reversible Computation. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271484⟩

Share

Metrics

Record views

122

Files downloads

52