線形で可逆な計算のためのカリー・ハワード対応

本論文では、帰納型と再帰を持つ線形で可逆なプログラミング言語を提案し、その言語とμMALLロジックの間のカリー・ハワード対応を示す。パターンマッチングのための構文的な網羅性と重複のなさが可逆性を保証することを示す。この言語は任意のプリミティブ再帰関数を表現できる。