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...

Descripción completa

Detalles Bibliográficos
Autores principales: Chardonnet, Kostia, Saurin, Alexis, Valiron, Benoît
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