A Curry-Howard Correspondence for Linear, Reversible Computation

TL;DR

This paper introduces a linear, reversible programming language with inductive types and recursion, establishing a Curry-Howard correspondence with a logic extended with fixed points, enabling representation of primitive recursive functions.

Contribution

It presents a novel reversible language with pattern-matching semantics and proves its correspondence with an extended linear logic, linking computation with logical proofs.

Findings

Language can represent all primitive recursive functions.

Reversibility is ensured by syntactical exhaustivity and non-overlapping clauses.

The language simulates cut-elimination in the logic $d$MALL.

Abstract

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic $\mu$MALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy $\mu$MALL validity criterion and how the language simulates the cut-elimination procedure of $\mu$MALL.