id	author	title	date	pages	extension	mime	words	sentences	flesch	summary	cache	txt
cord-028840-7n77vko9	Chardonnet, Kostia	Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress	2020-06-17		.txt	text/plain	2632	176	68	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. The constructors inj l and inj r represent the choice between either the left or right-hand side of a type of the form A ⊕ B; the constructor , builds pairs of elements (with the corresponding type constructor ⊗); fold and pack respectively represent inductive and coinductive structure for the types μX.A and νX.A. A value can serve both as a result and as a pattern in the clause of an iso. We presented a higher-order, linear, reversible language with inductive and coinductive types together with an interpretation of programs into derivations in the logic .	./cache/cord-028840-7n77vko9.txt	./txt/cord-028840-7n77vko9.txt