A specification logic for concurrent object-oriented programming

The paper focuses on the use of linear logic as a specification language of the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent-calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages whose corner-stone is the notion of {\em encapsulation}