Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets - extended abstract -

Didier Galmiche 1 Dominique Larchey-Wendling
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Linear logic is a logic of actions which seems well suited to various computer science applications. From its intrinsic ability to reflect computational resources, it is possible to refine different programming paradigms like formulae-as-types (proofs-as-programs) or formulae-as-states (proofs-as-computations) with a finer control on resource management. In the latter case, the correspondence between Intuitionistic Linear Logic (ILL) and Petri nets illustrates well the interest of efficient proof search methods for proving specifications or properties of distributed systems. In contrast to existing methods, for instance based on canonical proofs, we propose here to revisit the semantics of ILL and its interpretation on Petri nets to provide new proof techniques for proving or disproving properties. From a study of the relationships between the notions of ordered monoid and of quantale we define a new interpretation of ILL on Petri nets that is complete and verifies the property of finite models. Possible issues would be to derive a new algebraic semantics as basis of proof search and to propose a calculus to effectively build counter-models for ILL.
Type de document :
Article dans une revue
Electronic Notes in Theoretical Computer Science, Elsevier, 1998, 17, pp.1-18
Liste complète des métadonnées

https://hal.inria.fr/inria-00098605
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:03:53
Dernière modification le : mardi 24 avril 2018 - 13:34:34

Identifiants

  • HAL Id : inria-00098605, version 1

Collections

Citation

Didier Galmiche, Dominique Larchey-Wendling. Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets - extended abstract -. Electronic Notes in Theoretical Computer Science, Elsevier, 1998, 17, pp.1-18. 〈inria-00098605〉

Partager

Métriques

Consultations de la notice

114