The Structure of Interaction

Authors Stéphane Gimenez, Georg Moser



PDF
Thumbnail PDF

File

LIPIcs.CSL.2013.316.pdf
  • Filesize: 0.54 MB
  • 16 pages

Document Identifiers

Author Details

Stéphane Gimenez
Georg Moser

Cite AsGet BibTex

Stéphane Gimenez and Georg Moser. The Structure of Interaction. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 316-331, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.CSL.2013.316

Abstract

Interaction nets form a local and strongly confluent model of computation that is per se parallel. We introduce a Curry–Howard correspondence between well-formed interaction nets and a deep-inference deduction system based on linear logic. In particular, linear logic itself is easily expressed in the system and its computational aspects materialise though the correspondence. The system of interaction nets obtained is a typed variant of already well-known sharing graphs. Due to a strong confluence property, strong normalisation for this system follows from weak normalisation. The latter is obtained via an adaptation of Girard's reducibility method. The approach is modular, readily gives rise to generalisations (e.g. second order, known as polymorphism to the programmer) and could therefore be extended to various systems of interaction nets.
Keywords
  • Interaction Nets
  • Linear Logic
  • Curry–Howard Correspondence
  • Deep Inference
  • Calculus of Structures
  • Strong Normalisation
  • Reducibility

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail