### Program Extraction for Full Linear Logic

David Albrecht
Department of Computer Science, Monash University Clayton 3168, Australia.
dwa@bruce.cs.monash.edu.au

John N. Crossley
Department of Computer Science, Monash University Clayton 3168, Australia.
jnc@bruce.cs.monash.edu.au

John S. Jeavons
Department of Mathematics, Monash University Clayton 3168, Australia.
john.jeavons@maths.monash.edu.au

#### Abstract

In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. prove strong normalization for the system, and 4. prove that given a proof of $\forall x\exists y\ \alpha(x,y)$ and any individual term $t$ we can compute a term $u$ such that $\alpha(t,u)$ is provable.