Controlling program extraction in Elementary Linear Logic

TL;DR

This paper introduces a system based on elementary linear logic that enables the extraction of programs with guaranteed elementary time normalization, allowing higher-order specifications and implementation of all elementary recursive functions.

Contribution

It adapts Krivine & Leivant's FA_2 system for program extraction in elementary linear logic, enabling higher-order specifications and implementation of all elementary recursive functions.

Findings

Programs normalize in elementary time

All elementary recursive functions can be implemented

System allows higher-order equations as axioms

Abstract

We present an adaptation, based on program extraction in elementary linear logic, of Krivine & Leivant's system FA_2. This system allows to write higher-order equations in order to specify the computational content of extracted programs. The user can then prove a generic formula, using these equations as axioms, whose proof can be extracted into programs that normalize in elementary time and satisfy the specifications. Finally, we show that every elementary recursive functions can be implemented in this system.