New foundations for the geometry of interaction
- 2 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 74, 211-222
- https://doi.org/10.1109/lics.1992.185534
Abstract
A new formal embodiment of J.-Y. Girard's (1989) geometry of interaction program is given. The geometry of interaction interpretation considered is defined, and the computational interpretation is sketched in terms of dataflow nets. Some examples that illustrate the key ideas underlying the interpretation are given. The results, which include the semantic analogue of cut-elimination, stated in terms of a finite convergence property, are outlined.Keywords
This publication has 9 references indexed in Scilit:
- Notions of computation and monadsInformation and Computation, 1991
- Domain theory in logical form*Annals of Pure and Applied Logic, 1991
- Types in lambda calculi and programming languagesLecture Notes in Computer Science, 1990
- Data types in distributive categoriesBulletin of the Australian Mathematical Society, 1989
- Towards a geometry of interactionContemporary Mathematics, 1989
- Linear logicTheoretical Computer Science, 1987
- Categories of partial morphisms and the λP-calculusPublished by Springer Nature ,1986
- Algebraic semanticsLecture Notes in Computer Science, 1981
- Initial Algebra Semantics and Continuous AlgebrasJournal of the ACM, 1977