Skip to Main content Skip to Navigation
Journal articles

A Specification Logic for Concurrent Object-oriented Programming

Didier Galmiche 1 Giorgio Delzanno Maurizio Martelli
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This 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 encapsulation.
Document type :
Journal articles
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:41:00 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00098988, version 1



Didier Galmiche, Giorgio Delzanno, Maurizio Martelli. A Specification Logic for Concurrent Object-oriented Programming. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 1999, 9 (3), pp.253-286. ⟨inria-00098988⟩



Record views