In the paper we consider a proof-theoretical approach to Linear Logic in order to develop formal methods to specify computational aspects of concurrency and object-orientation. This paradigms enjoy complex operational mechanisms which require powerful frameworks in which they can be completely described. Thus, our passage from Classical to Linear Logic is motivated by the need of a more expressive language and deduction system.