Abstract
We introduce S2, a typed intermediate language for vectors, based on a 2-level type-theory, which distinguishes between compile-time and run-time. The paper shows how S2 can be used to extract useful information from programs written in the Nested Sequence Calculus NSC, an idealized high-level parallel calculus for nested sequences. We study two translations from NSC to S2. The most interesting shows that shape analysis (in the sense of Jay) can be handled at compile-time.
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
L. Birkedal, M. Tofte, and M. Vejlstrup. From Region Inference to von Neumann Machines via Region Representation Inference. In Proceedings from the 23rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1996.
G.E. Blelloch, S. Chatterjee, J.C. Hardwick, J. Sipelstein, and M. Zagha. Implementation of a portable nested data-parallel language. Journal of Parallel and Distributed Computing, 21(1), April 1994.
G.E. Blelloch and J. Greiner. A provable time and space efficient implementation of NESL. In ACM SIGPLAN International Conference on Functional Programming, pages 213–225, May 1996.
A. Carboni, S. Lack, and R.F.C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84:145–158, 1993.
T. Coquand and C. Paulin-Mohring. Inductively defined types. volume 389, LNCS, 1989.
R. Davies. A temporal-logic approach to binding-time analysis. In E. Clarke, editor, Proceedings of the Elenventh Annual Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.
H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.
R. Harper, J. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In 17th POPL. ACM, 1990.
R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 130–141, San Francisco, California, January 1995.
M. Hofmann. Dependent types: Syntax, semantics, and applications. Summer School on Semantics and Logics of Computation, University of Cambridge, Newton Institute for Mathematical Sciences, September 1995.
B. Jacobs, E. Moggi, and T. Streicher. Relating models of impredicative type theories. In Proceedings of the Conference on Category Theory and Computer Science, Manchester, UK, Sept. 1991, volume 389 of LNCS. Springer Verlag, 1991.
B.P.F. Jacobs. Categorical Type Theory. PhD thesis, University of Nijmegen, 1991.
C.B. Jay. Matrices, monads and the fast fourier transform. In Proceedings of the Massey Functional Programming Workshop 1994, pages 71–80, 1994.
C.B. Jay. A semantics for shape. Science of Computer Programming, 25:251–283, 1995.
C.B. Jay. Shape in computing. ACM Computing Surveys, 28(2):355–357, 1996.
C.B. Jay and M. Sekanina. Shape checking of array programs. In Computing: the Australasian Theory Seminar, Proceedings, 1997, 1997. accepted for publication.
E. Moggi. A category-theoretic account of program modules. Math. Struct. in Computer Science, 1:103–139, 1991.
F. Nielson and H.R. Nielson. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.
B. Nordström, K. Petersson, and J.M. Smith. Programming in Martin-Löf's type theory:an introduction. Number 7 in International series of monographs on computer science. Oxford University Press, New York, 1990.
S. Peyton Jones. Unboxed values as first-class citizens. In Functional Programming and Computer Architecture, volume 523 of LNCS, 1991.
A.M. Pitts. Notes on categorical logic. University of Cambridge, Computer Laboratory, Lent Term 1989.
D. Suciu and V. Tannen. Efficient compilation of high-level data parallel al-gorithms. In Proc. ACM Symposium on Parallel Algorithms and Architectures, June 1994.
J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2):245–296, June 1994.
M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value lambdacalculus using a stack of regions. In Proceedings from the 21st annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bellè, G., Moggi, E. (1997). Typed intermediate languages for shape analysis. In: de Groote, P., Roger Hindley, J. (eds) Typed Lambda Calculi and Applications. TLCA 1997. Lecture Notes in Computer Science, vol 1210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62688-3_26
Download citation
DOI: https://doi.org/10.1007/3-540-62688-3_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62688-6
Online ISBN: 978-3-540-68438-1
eBook Packages: Springer Book Archive