eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
316
331
10.4230/LIPIcs.CSL.2013.316
article
The Structure of Interaction
Gimenez, Stéphane
Moser, Georg
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.316/LIPIcs.CSL.2013.316.pdf
Interaction Nets
Linear Logic
Curry–Howard Correspondence
Deep Inference
Calculus of Structures
Strong Normalisation
Reducibility