###
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.

Conference Home Page