Abstract
The question we want to investigate was expressed by Girard in [3]:
“Assume that I am given a program P [a proof-net II], and that I cut it in two parts arbitrarily. I create two ... modules, linked together by their border. Can I express that my two modules are complementary [orthogonal], in other terms that I can branch them by identification over their common border? One would like to define the type of the modules as their branching instructions; these branching instructions should be such that they authorized the restoring of the original P [the proof-net II].”
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
V.M. Abrusci and P. Ruet. Non-commutative logic I: the multiplicative fragment. Università di Roma Tre and McGill University Preprints, 1998.
V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.
J.-Y. Girard. Multiplicatives. In Logic and Computer Science: new trends and applications (Lolli Editor), pages 11–34. Rendiconti del Seminario Matematico dell’Università e Politecnico di Torino, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michele Abrusci, V. (1999). Modules in Non-commutative Logic. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_3
Download citation
DOI: https://doi.org/10.1007/3-540-48959-2_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65763-7
Online ISBN: 978-3-540-48959-7
eBook Packages: Springer Book Archive