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.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 1999, 9 (3), pp.253-286
Liste complète des métadonnées

https://hal.inria.fr/inria-00098988
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:41:00
Dernière modification le : mardi 24 avril 2018 - 13:55:00

Identifiants

  • HAL Id : inria-00098988, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

88