Abstract
In the ambient logic of classical second order propositional calculus, we solve the specification problem for a family of excluded middle like tautologies. These are shown to be realized by sequential simulations of specific communication schemes for which they provide a safe typing mechanism.
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. Danos, J.-B. Joinet, H. Schellinx. A New Deconstructive Logic: Linear Logic (1996). Journal of Symbolic Logic.
J.-Y. Girard. A New Constructive Logic: Classical Logic (1992). Mathematical Structures in Computer Science.
T. Griffin. A formulae-as-types notion of control (1990). In Proceedings of POPL’90.
J.-L. Krivine. Typed Lambda-Calculus and Classical ZF Set-Theory (2000). Archive for Mathematical Logic.
L. Ong, C. Stewart. A Curry-Howard Foundation for Functional Computation with Control(1997). In Proceedings of POPL’97.
M. Parigot. Strong Normalization for Second-Order Lambda-Mu Calculus (1993). In Proceedings of LICS’93.
Moscova Project. The Join-Calculus Language: http://pauillac.inria.fr/join/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danos, V., Krivine, JL. (2000). Disjunctive Tautologies as Synchronisation Schemes. In: Clote, P.G., Schwichtenberg, H. (eds) Computer Science Logic. CSL 2000. Lecture Notes in Computer Science, vol 1862. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44622-2_19
Download citation
DOI: https://doi.org/10.1007/3-540-44622-2_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67895-3
Online ISBN: 978-3-540-44622-4
eBook Packages: Springer Book Archive