{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:29Z","timestamp":1742617229497,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_26","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:48:57Z","timestamp":1330296537000},"page":"11-29","source":"Crossref","is-referenced-by-count":1,"title":["Typed intermediate languages for shape analysis"],"prefix":"10.1007","author":[{"given":"Gianna","family":"Bell\u00e8","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eugenio","family":"Moggi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/237721.237771"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1006\/jpdc.1994.1038"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013225, May 1996.","DOI":"10.1145\/232627.232650"},{"key":"2_CR4","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0022-4049(93)90035-R","volume":"84","author":"A. Carboni","year":"1993","unstructured":"A. Carboni, S. Lack, and R.F.C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84:145\u2013158, 1993.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"T. Coquand and C. Paulin-Mohring. Inductively defined types. volume 389, LNCS, 1989.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"2_CR6","volume-title":"A temporal-logic approach to binding-time analysis","author":"R. Davies","year":"1996","unstructured":"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."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.","DOI":"10.1007\/BFb0014053"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"R. Harper, J. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In 17th POPL. ACM, 1990.","DOI":"10.1145\/96709.96744"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013141, San Francisco, California, January 1995.","DOI":"10.1145\/199448.199475"},{"key":"2_CR10","unstructured":"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."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/BFb0013467"},{"key":"2_CR12","unstructured":"B.P.F. Jacobs. Categorical Type Theory. PhD thesis, University of Nijmegen, 1991."},{"key":"2_CR13","unstructured":"C.B. Jay. Matrices, monads and the fast fourier transform. In Proceedings of the Massey Functional Programming Workshop 1994, pages 71\u201380, 1994."},{"key":"2_CR14","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0167-6423(95)00015-1","volume":"25","author":"C.B. Jay","year":"1995","unstructured":"C.B. Jay. A semantics for shape. Science of Computer Programming, 25:251\u2013283, 1995.","journal-title":"Science of Computer Programming"},{"issue":"2","key":"2_CR15","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1145\/234528.234749","volume":"28","author":"C.B. Jay","year":"1996","unstructured":"C.B. Jay. Shape in computing. ACM Computing Surveys, 28(2):355\u2013357, 1996.","journal-title":"ACM Computing Surveys"},{"key":"2_CR16","unstructured":"C.B. Jay and M. Sekanina. Shape checking of array programs. In Computing: the Australasian Theory Seminar, Proceedings, 1997, 1997. accepted for publication."},{"key":"2_CR17","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1017\/S0960129500000074","volume":"1","author":"E. Moggi","year":"1991","unstructured":"E. Moggi. A category-theoretic account of program modules. Math. Struct. in Computer Science, 1:103\u2013139, 1991.","journal-title":"Math. Struct. in Computer Science"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"F. Nielson and H.R. Nielson. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511526572"},{"key":"2_CR19","volume-title":"Number 7 in International series of monographs on computer science","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J.M. Smith. Programming in Martin-L\u00f6f's type theory:an introduction. Number 7 in International series of monographs on computer science. Oxford University Press, New York, 1990."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"S. Peyton Jones. Unboxed values as first-class citizens. In Functional Programming and Computer Architecture, volume 523 of LNCS, 1991.","DOI":"10.1007\/3540543961_30"},{"key":"2_CR21","unstructured":"A.M. Pitts. Notes on categorical logic. University of Cambridge, Computer Laboratory, Lent Term 1989."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.21236\/ADA290362"},{"issue":"2","key":"2_CR23","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J.-P. Talpin","year":"1994","unstructured":"J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2):245\u2013296, June 1994.","journal-title":"Information and Computation"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/174675.177855"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:31:30Z","timestamp":1742599890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}