Resources, Labels and Proofs

Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this talk, we focus on resource logics for modelling systems and programs and on theorem proving in such logics. Resource is a basic notion in computer science and location, access to, consumption of resources are central concerns in the design of correct systems (like networks) and programs (acces to memory, data structures manipulation). We show how the use of algebra of labels solves problems like resource distribution in theorem proving in resource logics, the labels being the elements of resource models. We illustrate the main points of this approach within the logic of bunched implications BI and present labelled calculi that are complete w.r.t. resource semantics and provide proofs or countermodels of BI formulae. The relationships between resource semantics, labels and proof calculi are central in this work.
Type de document :
Communication dans un congrès
Theory and Application of Abstract State Machines 2002, 2002, Schloss Dagstuhl, Wadern/Germany, 2002
Liste complète des métadonnées

https://hal.inria.fr/inria-00100789
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:51:03
Dernière modification le : mardi 24 avril 2018 - 13:32:49

Identifiants

  • HAL Id : inria-00100789, version 1

Collections

Citation

Didier Galmiche. Resources, Labels and Proofs. Theory and Application of Abstract State Machines 2002, 2002, Schloss Dagstuhl, Wadern/Germany, 2002. 〈inria-00100789〉

Partager

Métriques

Consultations de la notice

120