Article

Free access

The geometry of interaction machine

Author:

Ian MackieAuthors Info & Claims

POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 198 - 208

https://doi.org/10.1145/199448.199483

Published: 25 January 1995 Publication History

Abstract

We investigate implementation techniques arising directly from Girard's Geometry of Interaction semantics for Linear Logic, specifically for a simple functional programming language (PCF). This gives rise to a very simple, compact, compilation schema and run-time system. We analyse various properties of this kind of computation that suggest substantial optimisations that could make this paradigm of implementation not only practical, but potentially more efficient than extant paradigms.

References

[1]

Andrea Asperti, Vincent Danos, Cosimo Laneve, and Laurent Regnier. Paths in the A-calculus: Three years of communication without understanding. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 426-436. IEEE Computer Society Press, 1994.

[2]

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF (extended abstract). In Masami Hagiya and John C. Mitchel, editors, Theoretical Aspects of Computer Software. International Symposium TACS'9#, number 789 in Lecture Notes in Computer Science, pages 1-15, Sendai, Japan, April 1994. Springer-Verlag.

[3]

Andrea Asperti and Cosimo Laneve. Interaction systems I: The theory of optimal reductions. TechnicM Report 1748, INRIA Rocquencourt, 1991.

[4]

Andrea Asperti and Cosimo Laneve. Interaction systems II: The practice of optimal reductions. Technical Report UBLCS-93-12, Laboratory for Computer Science, University of Bologna, May 1993.

Digital Library

[5]

Vincent Danos. Une Applicat,on de la Logique Lindaire d l@tude des Processus de Normalisat,on (princ#palement du A-ealcul). PhD thesis, Universit# Paris VII, June 1990.

[6]

Vincent Danos and Laurent Regnier. Local and asynchronous beta-reduction (an analysis of Girard's execution formula). In Proceedings, Eighth Annual IEEE Symposium on Logic zn Computer Science, pages 296-306. IEEE Computer Society Press, 1993.

[7]

Anthony J. Field and Peter G. Harrison. Functional Programming. Addison Wesley, 1988.

[8]

Georges Gonthier, Martfn Abadi, and Jean- Jacques L6vy. The geometry of optimal lambda reduction. In Proceedings of A CM Symposium Princ,ples of Programming Languages, pages 15- 26, January 1992.

Digital Library

[9]

Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50(1):1-102, 1987.

Digital Library

[10]

Jean-Yves Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro et al., ed# itor, Logzc Colloquium 88. North Holland, 1989.

[11]

Jean-Yves Girard. Towards a geometry of interaction. In J. W. Gray and Andre Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 69-108. American Mathematical Society, 1989.

[12]

Yves Lafont. Interaction nets. In Proceedings of the Seventeenth A CM Symposium on Principles of Programming Languages, pages 95-108. ACM, ACM Press, January 1990.

Digital Library

[13]

Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6:308-320, 1964.

[14]

Jean-Jacques Levy. Optimal reductions in the lambda calculus. In J.P. Hindley and J.R Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 159-191. Academic Press, 1980.

[15]

Inn Mackie. The Geometry of Implementation. PhD thesis, Department of Computing, Imperim College of Science Technology and Medicine, 1994.

[16]

Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice Hall International, 1987.

Digital Library

[17]

Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.

[18]

Christopher P. Wadsworth. Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, Oxford University, 1971.

Cited By

Castellan SClairambault P(2023)The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal UnfoldingProceedings of the ACM on Programming Languages10.1145/35712177:POPL(689-717)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571217
Winskel G(2023)Making Concurrency Functional2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175727(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175727
Accattoli BGuerrieri G(2022)The theory of call-by-value solvabilityProceedings of the ACM on Programming Languages10.1145/35476526:ICFP(855-885)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547652
Show More Cited By

Index Terms

The geometry of interaction machine

Recommendations

The Geometry of Interaction of Differential Interaction Nets
LICS '08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science

The Geometry of Interaction purpose is to give a semantic of proofs or programs accounting for their dynamics. The initial presentation, translated as an algebraic weighting of paths in proofnets, led to a better characterization of the \lambda-calculus ...
Towards a typed geometry of interaction

Girard's Geometry of Interaction (GoI) develops a mathematical framework for modelling the dynamics of cut elimination. We introduce a typed version of GoI, called Multiobject GoI for both multiplicative linear logic (MLL) and multiplicative exponential ...
Haptic interaction with virtual geometry on robotic touch surface
SA '14: SIGGRAPH Asia 2014 Emerging Technologies

Touch screens are rapidly penetrating our daily life. Even general users are enjoying various applications such as drawing sketches and playing games with their mobile phones. In particular, the improvement of graphics capabilities with large display ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1995

415 pages

ISBN:0897916921

DOI:10.1145/199448

Chairmen:
Ron K. Cytron
Washington Univ., St. Louis, MO
,
Peter Lee
Carnegie Mellon Univ., Pittsburgh, PA

Copyright © 1995 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 1995

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL95

Sponsor:

POPL95: 22nd ACM Symposium on Principles of Programming Languages

January 23 - 25, 1995

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

75
Total Citations
View Citations
1,171
Total Downloads

Downloads (Last 12 months)195
Downloads (Last 6 weeks)17

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Castellan SClairambault P(2023)The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal UnfoldingProceedings of the ACM on Programming Languages10.1145/35712177:POPL(689-717)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571217
Winskel G(2023)Making Concurrency Functional2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175727(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175727
Accattoli BGuerrieri G(2022)The theory of call-by-value solvabilityProceedings of the ACM on Programming Languages10.1145/35476526:ICFP(855-885)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547652
Barthe GCrubillé RDal Lago UGavazzo F(2022)On Feller continuity and full abstractionProceedings of the ACM on Programming Languages10.1145/35476516:ICFP(826-854)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547651
Accattoli BDal Lago UVanoni G(2022)Multi types and reasonable spaceProceedings of the ACM on Programming Languages10.1145/35476506:ICFP(799-825)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547650
Vasilenko EVazou NBarthe G(2022)Safe couplings: coupled refinement typesProceedings of the ACM on Programming Languages10.1145/35476436:ICFP(596-624)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547643
Yoon IZakowski YZdancewic S(2022)Formal reasoning about layered monadic interpretersProceedings of the ACM on Programming Languages10.1145/35476306:ICFP(254-282)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547630
Ko HChen LLin T(2022)Datatype-generic programming meets elaborator reflectionProceedings of the ACM on Programming Languages10.1145/35476296:ICFP(225-253)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547629
Keuchel SHuyghebaert SLukyanov GDevriese D(2022)Verified symbolic execution with Kripke specification monads (and no meta-programming)Proceedings of the ACM on Programming Languages10.1145/35476286:ICFP(194-224)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547628
Ramsey N(2022)Beyond Relooper: recursive translation of unstructured control flow to structured control flow (functional pearl)Proceedings of the ACM on Programming Languages10.1145/35476216:ICFP(1-22)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547621
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents