Abstract
In this paper we describe a Curry-like type system for graphs and extend it with uniqueness information to indicate that certain objects are only ‘locally accessible’. The correctness of type assignment guarantees that no external access on such an object will take place in the future. We prove that types are preserved under reduction (for both type systems) for a large class of rewrite systems. Adding uniqueness information provides a solution to two problems in implementations of functional languages: efficient space behaviour and interfacing with non-functional operations.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Achten P.M., J.H.G. van Groningen and M.J. Plasmeijer, High Level Specification of I/O in Functional Languages, in: Proc. of International Workshop on Functional Languages, Glasgow, UK, Springer Verlag, 1993.
Bakel S. van, S. Smetsers and S. Brock, Partial Type Assignment in Left-Linear Term Rewriting Systems, in: J.C. Raoult, editor, Proc. of 17th Colloqium on Trees and Algebra in Programming (CAAP'92), pages 300–322, Rennes, France, Springer Verlag, LNCS 581, 1992.
Barendregt H.P., M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer and M.R. Sleep, Towards an Intermediate Language based on Graph Rewriting, in: Proc. of Parallel Architectures and Languages Europe (PARLE), pages 159–175, Eindhoven, The Netherlands, Springer Verlag, LNCS 259 II, 1987.
Barendregt H.P., M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer and M.R. Sleep, Term Graph Reduction, in: Proc. of Parallel Architectures and Languages Europe (PARLE), pages 141–158, Eindhoven, The Netherlands, Springer Verlag, LNCS 259 II, 1987.
Barendsen Erik and Sjaak Smetsers, Graph Rewriting and Copying, Technical Report 92-20, University of Nijmegen, 1992.
Guzmán J.C. and P. Hudak, Single-Threaded Polymorphic Lambda Calculus, in: Proc. of 5th IEEE Symp. on Logic in Computer Science, pages 333–343, Philadelphia, PA, IEEE Computer Society Press, 1990.
Jacobs B.P.F., Conventional and Linear Formulas in a Logic of Coalgebras, Typescript, University of Utrecht, 1993.
Nöcker E.G.J.M.H., J.E.W. Smetsers, M.C.J.D. van Eekelen and M.J. Plasmeijer, Concurrent Clean, in: Proc. of Parallel Architectures and Languages Europe (PARLE'91), pages 202–219, Eindhoven, The Netherlands, Springer Verlag, LNCS 505, 1991.
Smetsers Sjaak, Erik Barendsen, Marko van Eekelen and Rinus Plasmeijer, Guaranteeing Safe Destructive Updates through a Type System with Uniqueness Information for Graphs, Technical report, University of Nijmegen, 1993.
Wadler P., Linear types can change the world!, in: Proc. of Working Conference on Programming Concepts and Methods, pages 385–407, Israel, North Holland, 1990.
Wadsworth C.P., Semantics and Pragmatics of the Lambda Calculus, PhD thesis, Oxford University, 1971.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barendsen, E., Smetsers, S. (1993). Conventional and uniqueness typing in graph rewrite systems. In: Shyamasundar, R.K. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1993. Lecture Notes in Computer Science, vol 761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57529-4_42
Download citation
DOI: https://doi.org/10.1007/3-540-57529-4_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57529-0
Online ISBN: 978-3-540-48211-6
eBook Packages: Springer Book Archive