Proofs as Executions - IFIP Open Digital Library Access content directly
Reports Year : 2011

Proofs as Executions

Virgile Mogbil
  • Function : Author
  • PersonId : 829467

Abstract

This paper proposes a new interpretation of the logical contents of programs in the context of concurrent interaction, wherein proofs correspond to successful executions of a processes. A type system based on linear logic is used, in which a given process may have several different types, each typing corresponding to a particular way of interacting with its environment, and cut elimination corresponds to executing the process in a given scenario. We prove that, for any process, the set of lock-avoiding executions precisely corresponds to the set of typings of the process. Particularly important is the role played by the axiom rule, which allows typings to make assumptions on the events of the environment. In this interpretation, logic appears as a way of making explicit the flow of causality between interacting processes.
Fichier principal
Vignette du fichier
pase_preprintLIPN11.pdf (225.3 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-00586459 , version 1 (16-04-2011)
hal-00586459 , version 2 (25-05-2012)

Identifiers

  • HAL Id : hal-00586459 , version 1

Cite

Emmanuel Beffara, Virgile Mogbil. Proofs as Executions. 2011. ⟨hal-00586459v1⟩
515 View
171 Download

Share

Gmail Facebook X LinkedIn More