Proofs as computations in linear logic