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