A typed calculus based on a fragment of linear logic