Cargando…
Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress
In this paper, we present a linear and reversible language with inductive and coinductive types, together with a Curry-Howard correspondence with the logic [Image: see text] : linear logic extended with least and greatest fixed points allowing inductive and coinductive statements. Linear, reversible...
Autores principales: | , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7342045/ http://dx.doi.org/10.1007/978-3-030-52482-1_8 |
_version_ | 1783555351133552640 |
---|---|
author | Chardonnet, Kostia Saurin, Alexis Valiron, Benoît |
author_facet | Chardonnet, Kostia Saurin, Alexis Valiron, Benoît |
author_sort | Chardonnet, Kostia |
collection | PubMed |
description | In this paper, we present a linear and reversible language with inductive and coinductive types, together with a Curry-Howard correspondence with the logic [Image: see text] : linear logic extended with least and greatest fixed points allowing inductive and coinductive 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. |
format | Online Article Text |
id | pubmed-7342045 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-73420452020-07-09 Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress Chardonnet, Kostia Saurin, Alexis Valiron, Benoît Reversible Computation Article In this paper, we present a linear and reversible language with inductive and coinductive types, together with a Curry-Howard correspondence with the logic [Image: see text] : linear logic extended with least and greatest fixed points allowing inductive and coinductive 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. 2020-06-17 /pmc/articles/PMC7342045/ http://dx.doi.org/10.1007/978-3-030-52482-1_8 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic. |
spellingShingle | Article Chardonnet, Kostia Saurin, Alexis Valiron, Benoît Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress |
title | Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress |
title_full | Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress |
title_fullStr | Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress |
title_full_unstemmed | Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress |
title_short | Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress |
title_sort | toward a curry-howard equivalence for linear, reversible computation: work-in-progress |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7342045/ http://dx.doi.org/10.1007/978-3-030-52482-1_8 |
work_keys_str_mv | AT chardonnetkostia towardacurryhowardequivalenceforlinearreversiblecomputationworkinprogress AT saurinalexis towardacurryhowardequivalenceforlinearreversiblecomputationworkinprogress AT valironbenoit towardacurryhowardequivalenceforlinearreversiblecomputationworkinprogress |