SPACE SEMANTICS, PROGRAM ANALYSIS, AND COMPUTING
ENVIRONMENTS FOR MEMORY MANAGEMENT
INDEX
o SPACE
o WORKSHOPS
o MAILING LIST
o PEOPLE
o BIBLIOGRAPHY

o ABOUT
H
H

BIBLIOGRAPHY

This bibliography covers SPACE-related literature up until 2001 compiled by Henning Niss. If you are interested in updating the bibliography, please send an email to henglein@diku.dk.

[1]
Samson Abramsky and Chris Hankin, editors. Abstract Interpretation of Declarative Languages. Ellis Horwood, 1987.
Key: ABSINT:87.
[2]
Alexander Aiken, Manuel Fähndrich, and Raph Levien. Better static memory management: Improving region-based analysis of higher-order languages. In PLDI [151], pages 174-185.
* Key: Aiken-Faehndrich-Levien:1995.
[3]
Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.
Key: Appel:1992.
[4]
Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca, editors. Proceedings of the 16th International Colloquium on Automata, Languages and Programming (ICALP), volume 372 of Lecture Notes in Computer Science, Stresa, Italy, July 1989. Springer-Verlag.
Key: ICALP:89.
[5]
Roland Backhouse and José Nuno Oliveira, editors. Proceedings of the Fifth International Conference on Mathematics of Program Construction (MPC), volume 1837 of Lecture Notes in Computer Science, Ponte de Lima, Portugal, July 2000. Springer-Verlag.
Key: MPC:2000.
[6]
Henry G. Baker. List processing in real-time on a serial computer. Communications of the ACM, 21(4):280-94, 1978.
Key: Baker:1978.
[7]
Henry G. Baker. Unify and conquer (garbage, updating, aliasing ...) in functional languages. In LFP [112], pages 218-226.
Key: Baker:1990.
[8]
Henry G. Baker, editor. Proceedings of the 1995 International Workshop on Memory Management (IWMM), number 986 in Lecture Notes in Computer Science, Kinross, Scotland, September 1995. Springer-Verlag.
Key: IWMM:95.
[9]
Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Region analysis and the polymorphic lambda calculus. In LICS [116], pages 88-97.
* Key: Banerjee-Heintze-Riecke:1999.
[10]
David A. Barrett and Benjamin G. Zorn. Using lifetime predictors to improve memory allocation performance. In PLDI [149], pages 187-196.
Key: Barrett-Zorn:1993.
[11]
Jeffrey M. Barth. Shifting garbage collection overhead to compile time. Communications of the ACM, 20(7):513-518, 1977.
Key: Barth:1977.
[12]
Yves Bekkers and Jacques Cohen, editors. Proceedings of the 1992 International Workshop on Memory Management (IWMM), number 637 in Lecture Notes in Computer Science, St. Malo, France, September 1992. Springer-Verlag.
Key: IWMM:92.
[13]
Michael Benedikt, Thomas Reps, and Mooly Sagiv. A decidable logic for describing linked data structures. In Swierstra [193], pages 2-19.
Key: Benedikt-Reps-Sagiv:1999.
[14]
Lars Birkedal, Nick Rothwell, Mads Tofte, and David N. Turner. The ML kit (version 1). Technical Report DIKU-TR-93/14, Department of Computer Science, University of Copenhagen (DIKU), 1993.
Key: Birkedal-al:1993.
[15]
Lars Birkedal and Mads Tofte. A constraint-based region inference algorithm. Theoretical Computer Science, 2000. To appear in TCS.
* Key: Birkedal-Tofte:2000.
[16]
Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. From region inference to von Neumann machines via region representation inference. In POPL [164], pages 171-183.
* Key: Birkedal-Tofte-Vejlstrup:1996.
[17]
Peter B. Bishop. Computer Systems with a Very Large Address Space and Garbage Collection. PhD thesis, Massachusetts Institute of Technology, Laboratory for Computer Science (MIT), 1977.
Key: Bishop:1977.
[18]
Michael R. Blair. A design for an efficient type/region/effect/kind checking system. Master's thesis, Massachusetts Institute of Technology, Laboratory for Computer Science (MIT), 1990.
Key: Blair:1990.
[19]
Richard Bornat. Proving pointer programs in Hoare logic. In Backhouse and Oliveira [5], pages 102-126.
* Key: Bornat:2000.
[20]
Stephen D. Brookes, Michael Main, Austin Melton, and Michael W. Mislove, editors. Proceedings of the Eleventh Annual Confernce on Mathematical Foundations of Programming Semantics (MFPS), volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.
Key: MFPS:1995.
[21]
Manfred Broy and Gunther Schmidt, editors. Theoretical Foundations of Programming Methodology. D. Reidel, 1982.
Key: MARKTOBERDORF:81.
[22]
Rod M. Burstall. Some techniques for proving correctness of programs which alter data structures. In B. Meltzer and D. Mitchie, editors, Machine Intelligence, volume 7, pages 23-50. Edinburgh University Press, 1972.
Key: Burstall:1972.
[23]
Cristiano Calcagno. Stratified operational semantics for safety and correctness of region calculus. In POPL [168], pages 155-165.
* Key: Calcagno:2001.
[24]
Cristiano Calcagno, Simon Helsen, and Peter Thiemann. Syntactic type soundness results for the region calculus. Information & Computation, To appear.
Key: Calcagno-Helsen-Thiemann:2001.
[25]
Cristiano Calcagno, Samin Ishtiaq, and Peter W. O'Hearn. Semantic analysis of pointer aliasing, allocation and disposal in hoare logic. In PPDP [169], pages 190-201.
* Key: Calcagno-Ishtiaq-OHearn:2000.
[26]
Jérôme Chailloux, Matthieu Devin, and Jean-Marie Hullot. LeLisp, a portable and efficient Lisp system. In LFP [110], pages 113-122.
Key: Chailloux-Devin-Hullot:1984.
[27]
David R. Chase. Safety considerations for storage allocation optimizations. In PLDI [146], pages 1-10.
Key: Chase:1988.
[28]
Jawahar Chirimar, Carl A. Gunter, and Jon G. Riecke. Proving memory management invariants for a language based on linear logic. In LFP [113], pages 139-150.
Key: Chirimar-Gunter-Riecke:1992.
[29]
Jawahar Chirimar, Carl A. Gunter, and Jon G. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2):195-244, 1996. Extended version of [29].
Key: Chirimar-Gunter-Riecke:1996.
[30]
Stephen A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1):70-90, February 1978.
Key: Cook:1978.
[31]
Stephen A. Cook and Derek C. Oppen. An assertion language for data structures. In POPL [157], pages 160-166.
Key: Cook-Oppen:1975.
[32]
Karl Crary, editor. The Third International Workshop on Types in Compilation (TIC). ??, September 2000.
Key: TIC:2000.
[33]
Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In POPL [166], pages 262-275.
* Key: Crary-Walker-Morrisett:1999.
[34]
Luís Manuel Martins Damas. Type Assignment in Programming Langugages. PhD thesis, University of Edinburgh, 1984.
Key: Damas:1984.
[35]
Manuvir Das. Unification-based pointer analysis with directional assignments. In PLDI [154], pages 35-46.
Key: Das:2000.
[36]
V. Delacour. Allocation regions and implementation contracts. In Bekkers and Cohen [12], pages 426-439.
* Key: Delacour:1992.
[37]
Alain Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In POPL [160], pages 157-168.
Key: Deutsch:1990.
[38]
Alain Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In PLDI [150], pages 230-241.
Key: Deutsch:1994.
[39]
Alain Deutsch. On the complexity of escape analysis. In POPL [165], pages 358-371.
Key: Deutsch:1997.
[40]
Edsger W. Dijkstra. Recursive programming. Numerische Mathematik, 2:312-318, 1960. Reprinted in [Rosen:1967].
Key: Dijkstra:1960.
[41]
J. Michael Dunn. Relevance logic and entailment. In Dov M. Gabbay and Franz Guenthner, editors, Handbook of Philosophical Logic, volume III (Alternatives to classical logic), chapter 3, pages 117-225. Reidel, Dordrecht, 1986.
Key: Dunn:1986.
[42]
Jacob Elgaard, Anders Møller, and Michael I. Schwartzbach. Compile-time debugging of C programs working on trees. In Smolka [185], pages 119-134.
* Key: Elgaard-Moeller-Schwartzbach:2000.
[43]
Martin Elsman. Program Modules, Separate Compilation, and Intermodule Optimisation. PhD thesis, Department of Computer Science, University of Copenhagen (DIKU), 1999.
* Key: Elsman:1999.
[44]
Martin Elsman and Niels Hallenberg. An optimizing backend for the ML Kit using a stack of regions. Student Project, Department of Computer Science, University of Copenhagen (DIKU), July 1995.
* Key: Elsman-Hallenberg:1995.
[45]
Manuel Fähndrich, Jakob Rehof, and Manuvir Das. Scalable context-sensitive flow analysis using instantiation constraints. In PLDI [154], pages 253-263.
Key: Faehndrich-Rehof-Das:2000.
[46]
Christian Ferdinand, Florian Martin, Reinhard Wilhelm, and Martin Alt. Cache behavior prediction by abstract interpretation. Science of Computer Programming, 35(2-3):163-189, 1999.
Key: Ferdinand-al:1999.
[47]
Christian Ferdinand and Reinhead Wilhelm. Efficient and precise cache behavior prediction for real-time systems. Real-Time Systems, 17(2-3):131-181, 1999.
Key: Ferdinand-Wilhelm:1999.
[48]
Robert W. Floyd. Assigning meanings to programs. In Jacob T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32. American Mathematical Society, 1967.
Key: Floyd:1967.
[49]
Jörg Flum and Mario Rodríguez-Artalejo, editors. 13th International Workshop on Computer Science Logic (CSL), volume 1683 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
Key: CSL:1999.
[50]
Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture (FPCA), La Jolla, California, June 1995. ACM Press.
Key: FPCA:95.
[51]
Pascal Fradet. Syntactic detection of single-threading using continuations. In Hughes [82], pages 241-258.
Key: Fradet:1991.
[52]
Pascal Fradet. Collecting more garbage. In LFP [114], pages 24-33.
Key: Fradet:1994.
[53]
Martin Gardner. The fantastic combinations of John Conway's new solitaire game ``life''. Scientific American, 223(3):120-123, 1970.
Key: Gardner:1970.
[54]
David Gay and Alexander Aiken. Memory management with explicit regions. In PLDI [153], pages 313-323.
* Key: Gay-Aiken:1998.
[55]
David Gay and Alexander Aiken. Language support for regions. In PLDI [155], pages 70-80.
Key: Gay-Aiken:2001.
[56]
David Gay and Bjarne Steensgaard. Fast escape analysis and stack allocation for object-based programs. In Watt [221], pages 82-93.
Key: Gay-Steensgaard:2000.
[57]
Michael Georgeff. Transformations and reduction strategies for typed lambda expressions. ACM Transactions on Programming Languages and Systems, 6(4):603-631, 1984.
Key: Georgeff:1984.
[58]
David K. Gifford, Pierre Jouvelot, John M. Lucassen, and Mark A. Sheldon. FX-87 reference manual. Technical Report MIT-LCS//MIT/LCS/TR-407, Massachusetts Institute of Technology, Laboratory for Computer Science (MIT), 1987.
Key: Gifford-al:1987.
[59]
David K. Gifford, Pierre Jouvelot, Mark A. Sheldon, and Jamoes W. O'Toole. Report on the FX programming language. Technical Report MIT-LCS//MIT/LCS/TR-531, Massachusetts Institute of Technology, Laboratory for Computer Science (MIT), 1992. An earlier report, on FX-87, appeared as [58].
* Key: Gifford-al:1992.
[60]
David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In LFP [111], pages 28-38.
* Key: Gifford-Lucassen:1986.
[61]
Jean-Yves Girard, editor. 4th International Conference on Typed Lambda Calculi and Applications (TLCA), volume 1581 of Lecture Notes in Computer Science, L'Aquila, Italy, April 1999. Springer-Verlag.
Key: TLCA:99.
[62]
GNU. GNU C library, version 2.0.6, 1998.
Key: gnu-libc.
[63]
Dirk Grunwald and Benjamin Zorn. CustoMalloc: Efficient, synthesised memory allocators. Software--Practice and Experience, 23:851-869, 1993.
Key: Grunwald-Zorn:1993.
[64]
Tibor Gyimóthy, editor. Proceedings of the Sixth International Conference on Compiler Construction (CC), volume 1060 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
Key: CC:96.
[65]
Niels Hallenberg. A region profiler for a Standard ML compiler based on region inference. Student Project, Department of Computer Science, University of Copenhagen (DIKU), June 1996.
* Key: Hallenberg:1996.
[66]
Niels Hallenberg. Combining garbage collection and region inference in the ML Kit. Master's thesis, Department of Computer Science, University of Copenhagen (DIKU), June 1999.
* Key: Hallenberg:1999.
[67]
Geoff W. Hamilton and Simon B. Jones. Compile-time garbage collection by necessity analysis. In Jones et al. [101], pages 66-70.
Key: Hamilton-Jones:1990.
[68]
David R. Hanson. Fast allocation and deallocation of memory based on object lifetimes. Software--Practice and Experience, 20(1):5-12, 1990.
* Key: Hanson:1990.
[69]
Barry Hayes. Using key object opportunism to collect old objects. In Paepcke [144], pages 33-46.
Key: Hayes:1991.
[70]
Simon Helsen. An operational theory for a region calculus. Unpublished draft, November 2001.
Key: Helsen:2001.
[71]
Simon Helsen and Peter Thiemann. Syntactic type soundness for the region calculus. In Alan Jeffrey, editor, ACM Workshop on Higher Order Operational Techniques in Semantics, volume 41(3) of Electronic Notes in Theoretical Computer Science, pages 1-20. Elsevier, September 2000.
* Key: Helsen-Thiemann:2000.
[72]
Laurie J. Hendren, Joseph Hummel, and Alexandru Nicolau. Abstractions for recursive pointer data structures: Improving the analysis and transformation of imperative programs. In PLDI [148], pages 249-260.
Key: Hendren-Hummel-Nicolau:1992.
[73]
Fritz Henglein, John Hughes, Henning Makholm, and Henning Niss, editors. Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE), London, UK, 15-16 January 2001. IT University of Copenhagen.
Key: SPACE:2001.
[74]
Fritz Henglein, Henning Makholm, and Henning Niss. A direct approach to control-flow sensitive region-based memory management. In PPDP [170], pages ??--??
Key: Henglein-Makholm-Niss:2001a.
[75]
Fritz Henglein, Henning Makholm, and Henning Niss. A direct approach to control-flow sensitive region-based memory management (extended version). Technical report, Department of Computer Science, University of Copenhagen (DIKU), 2001. http://www.diku.dk/~hniss/rbmm/ppdp-ext.ps.gz.
Key: Henglein-Makholm-Niss:2001b.
[76]
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969.
Key: Hoare:1969.
[77]
Martin Hofmann. A type system for bounded space and functional in-place update (extended abstract). In Smolka [185], pages 165-179.
Key: Hofmann:2000.
[78]
Antony Hosking, editor. Proceedings of the 2000 ACM International Symposium on Memory Management (ISMM), volume 36(3) of SIGPLAN Notices. ACM Press, October 2000.
Key: ISMM:2000.
[79]
Haruo Hosoya and Akinori Yonezawa. Garbage collection via dynamic type inference --- a formal treatment. In Leroy and Ohori [109], pages 215-239.
Key: Hosoya-Yonezawa:1998.
[80]
Paul R. Hudak. A semantic model of reference counting and its abstraction. In LFP [111], pages 351-363.
Key: Hudak:1986.
[81]
Paul R. Hudak. A semantic model of reference counting and its abstraction. In Abramsky and Hankin [1], pages 45-62. Extended version of [80].
Key: Hudak:1987.
[82]
John Hughes, editor. Proceedings of the Fifth ACM Conference on Functional Programming and Computer Architecture (FPCA), number 523 in Lecture Notes in Computer Science, Cambridge, Massachusetts, August 1991. Springer-Verlag.
Key: FPCA:91.
[83]
John Hughes and Lars Pareto. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In ICFP [86], pages 70-81.
* Key: Hughes-Pareto:1999.
[84]
John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In POPL [164], pages 410-423.
Key: Hughes-Pareto-Sabry:1996.
[85]
Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming (ICFP), volume 34(1) of SIGPLAN Notices, Baltimore, Maryland, September 1998. ACM Press.
Key: ICFP:98.
[86]
Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP), volume 34(9) of SIGPLAN Notices, Paris, France, September 1999. ACM Press.
Key: ICFP:99.
[87]
Atsushi Igarashi and Naoki Kobayashi. Garbage collection based on a linear type system. In Crary [32], page ??
Key: Igarashi-Kobayashi:2000.
[88]
Katsuro Inoue, Hiroyuki Seki, and Hikaru Yagi. Analysis of functional programs to detect run-time garbage cells. ACM Transactions on Programming Languages and Systems, 10(4):555-578, 1988.
Key: Inoue-Seki-Yagi:1988.
[89]
Samin Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In POPL [168], pages 14-26.
* Key: Ishtiaq-OHearn:2001.
[90]
Samin S. Ishtiaq and David J. Pym. Kripke resource models of a dependently-typed, bunched lambda-calculus. In Flum and Rodríguez-Artalejo [49], pages 235-249.
* Key: Ishtiaq-Pym:1999.
[91]
Simon B. Jones Jean-Pierre Banâtre and Daniel Le Métayer, editors. Prospects for Functional Programming in Software Engineering. Springer-Verlag, 1991.
Key: ESPRIT:91.
[92]
Jacob L. Jensen, Michael E. Jørgensen, Nils Klarlund, and Michael I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In PLDI [152], pages 226-236.
Key: Jensen-al:1997.
[93]
Thomas P. Jensen and Torben Æ. Mogensen. A backwards analysis for compile-time garbage collection. In Jones [95], pages 227-239.
Key: Jensen-Mogensen:1990.
[94]
Jim Woodcock Jim Davies, Bill Roscoe, editor. Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare. Palgrave, 2000.
Key: MILLENNIAL:2000.
[95]
Neil D. Jones, editor. Proceedings of the Third European Symposium on Programming (ESOP), volume 432 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
Key: ESOP:90.
[96]
Neil D. Jones and Steven S. Muchnick. Flow analysis and optimization of Lisp-like structures. In Muchnick and Jones [130], pages 102-131.
Key: Jones-Muchnick:1981.
[97]
Richard Jones, editor. Proceedings of the 1998 ACM International Symposium on Memory Management (ISMM), volume 34(3) of SIGPLAN Notices. ACM Press, October 1998.
Key: ISMM:98.
[98]
Richard Jones and Rafael Lins. Garbage collection: Algorithms for Automatic Dynamic Memory Management. John Wiley, New York, USA, 1996.
Key: Jones-Lins:1996.
[99]
Simon B. Jones and Daniel Le Métayer. Compile-time garbage collection by sharing analysis. In Stoy [190], pages 54-74.
Key: Jones-Metayer:1989.
[100]
Simon B. Jones and Daniel Le Métayer. Compile-time garbage collection by sharing analysis. In Jean-Pierre Banâtre and Métayer [91], chapter 4, pages 59-86. Extended version of [99].
Key: Jones-Metayer:1991.
[101]
Simon L. Peyton Jones, Graham Hutton, and Carsten Kehler Holst, editors. Proceedings of the 1990 Glasgow Workshop on Functional Programming, Workshops in Computing, Glasgow, Scotland, August 1991. Springer-Verlag.
Key: GWF:90.
[102]
Pierre Jouvelot and David K. Gifford. Reasoning about continuations with control effects. In PLDI [147], pages 218-226.
* Key: Jouvelot-Gifford:1989.
[103]
Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In POPL [161], pages 303-310.
* Key: Jouvelot-Gifford:1991.
[104]
Nils Klarlund and Michael I. Schwartzbach. Graph types. In POPL [162], pages 196-205.
* Key: Klarlund-Schwartzbach:1993.
[105]
Martin Koch and Tommy Højfeld Olesen. Compiling a higher-order call-by-value functional programming language to a RISC using a stack of regions. Master's thesis, Department of Computer Science, University of Copenhagen (DIKU), 1996.
* Key: Koch-Olesen:1996.
[106]
Bernd Krieg-Brückner, editor. Proceedings of the Fourth European Symposium on Programming (ESOP), number 582 in Lecture Notes in Computer Science, Rennes, France, February 1992. Springer-Verlag.
Key: ESOP:92.
[107]
Butler Lampson. A description of the Cedar language. Technical Report CSL-83-15, Xerox PARC, December 1983.
Key: Lampson:1983.
[108]
Xavier Leroy. Polymorphic Typing of an Algorithmic Language. PhD thesis, Université Paris VII, INRIA, 1992. English translation of a french doctoral dissertation.
Key: Leroy:1992.
[109]
Xavier Leroy and Atsushi Ohori, editors. The Second International Workshop on Types in Compilation (TIC), number 1473 in Lecture Notes in Computer Science. Springer-Verlag, March 1998.
Key: TIC:98.
[110]
Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming (LFP), Austin, Texas, August 1984. ACM Press.
Key: LFP:84.
[111]
Proceedings of the 1986 ACM Conference on Lisp and Functional Programming (LFP), Cambridge, Massachusetts, August 1986. ACM Press.
Key: LFP:86.
[112]
Proceedings of the 1990 ACM Conference on Lisp and Functional Programming (LFP), Nice, France, June 1990. ACM Press.
Key: LFP:90.
[113]
Proceedings of the 1990 ACM Conference on Lisp and Functional Programming (LFP), San Francisco, California, June 1990. ACM Press.
Key: LFP:92.
[114]
Proceedings of the 1994 ACM Conference on Lisp and Functional Programming (LFP), Orlando, Florida, June 1994. ACM Press.
Key: LFP:94.
[115]
Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS), Santa Cruz, California, June 1992. IEEE Computer Society Press.
Key: LICS:92.
[116]
Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, July 1999. IEEE Computer Society Press.
Key: LICS:99.
[117]
Henry Lieberman and Carl E. Hewitt. A real-time garbage collector based on the lifetimes of objects. Communications of the ACM, 26(6):419-429, 1983.
Key: Lieberman-Hewitt:1983.
[118]
Jacques Loeckx, Kurt Sieber, and Ryan D. Stansifer. The Foundations of Program Verification. John Wiley, second edition, 1987.
Key: Loeckx-Sieber-Stansifier:1987.
[119]
John M. Lucassen. Types and Effects: Towards the Integration of Functional and Imperative Programming. PhD thesis, Massachusetts Institute of Technology, Laboratory for Computer Science (MIT), 1987.
Key: Lucassen:1987.
[120]
John M. Lucassen and David K. Gifford. Polymorphic effect systems. In POPL [159], pages 47-57.
* Key: Lucassen-Gifford:1988.
[121]
Henning Makholm. Region-based memory management in Prolog. Master's thesis, Department of Computer Science, University of Copenhagen (DIKU), March 2000. DIKU Technical Report 00/09.
Key: Makholm:2000a.
[122]
Henning Makholm. A region-based memory manager for Prolog. In Hosking [78], pages 25-34.
Key: Makholm:2000b.
[123]
Robin Milner, Mads Tofte, Robert Harper, and David B. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
Key: Milner-al:1997.
[124]
ML Kit webpage, 2001. url http://www.it-c.dk/research/mlkit.
Key: MLKit-webpage.
[125]
Stefan Monnier, Bratin Saha, and Zhong Shao. Principled scavenging. Technical Report YALEU/DCS/TR-1205, Dept. of Computer Science, Yale University, New Haven, CT, 2000.
Key: Monnier-Saha-Shao:2000.
[126]
Ugo Montanari, José D. P. Rolim, and Emo Welzl, editors. Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP), volume 1853 of Lecture Notes in Computer Science, Geneva, Switzerland, July 2000. Springer-Verlag.
Key: ICALP:2000.
[127]
Joseph M. Morris. Assignment and linked data structures. In Broy and Schmidt [21], pages 35-41.
Key: Morris:1981b.
[128]
Joseph M. Morris. A general axiom of assignment. In Broy and Schmidt [21], pages 25-34.
Key: Morris:1981a.
[129]
Joseph M. Morris. A proof of the Schorr-Waite algorithm. In Broy and Schmidt [21], pages 43-51.
Key: Morris:1981c.
[130]
Steven S. Muchnick and Neil D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.
Key: MUCHNICK-JONES:81.
[131]
Alan Mycroft and Richard W. Sharp. A statically allocated parallel functional language. In Montanari et al. [126], pages 37-48.
Key: Mycroft-Sharp:2000.
[132]
Peter Naur. Proof of algorithms by general snapshots. BIT, 6:310-316, 1966.
Key: Naur:1966.
[133]
Anne Neirynck, Prakash Panangaden, and Alan J. Demers. Effect analysis in higher-order languages. International Journal of Parallel Programming, 18(1):1-36, 1989.
Key: Neirynck-Panangaden-Demers:1989.
[134]
Mogens Nielsen and Branislav Rovan, editors. Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science, volume 1893 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
Key: MFCS:2000.
[135]
Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: A Formal Introduction. John Wiley, 1992. Currently not available from the publisher, but a revised edition is available from url http://www.daimi.au.dk/ bra8130/Wiley_book/wiley.html.
Key: Nielson-Nielson:1992.
[136]
Peter W. O'Hearn. Resource interpretations, bunched implications and the alpha - lambda -calculus. In Girard [61], pages 258-279.
Key: OHearn:1999.
[137]
Peter W. O'Hearn, A. John Power, Makato Takeyama, and Robert D. Tennent. Syntactic control of interference revisited. In Brookes et al. [20]. Superseded by [138].
Key: OHearn-al:1995.
[138]
Peter W. O'Hearn, A. John Power, Makato Takeyama, and Robert D. Tennent. Syntactic control of interference revisited. Theoretical Computer Science, 228(1-2):211-252, 1999. Extended version of [137].
Key: OHearn-al:1999.
[139]
Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999.
* Key: OHearn-Pym:1999.
[140]
Peter W. O'Hearn, David J. Pym, and Hongseok Yang. Possible worlds and resources: The semantics of BI. Draft manuscript, 2000.
* Key: OHearn-Pym-Yang:2000.
[141]
Peter W. O'Hearn and Robert D. Tennent, editors. ALGOL-like Languages. Birkhäuser, 1997. Two volumes.
Key: OHearn-Tennent:1997.
[142]
Peter W. O'Hearn and Hongseok Yang. Local reasoning about pointer programs using bunched implication. In preparation, 2000.
Key: OHearn-Yang:2000.
[143]
Derek C. Oppen and Stephen A. Cook. Proving assertions about programs that manipulate data structures. In STOC [188], pages 107-116.
Key: Oppen-Cook:1975.
[144]
Andreas Paepcke, editor. Proceeings of the 1991 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages & Applications (OOPSLA), volume 26(11) of SIGPLAN Notices, Phoenix, Arizona, November 1991. ACM Press.
Key: OOPSLA:91.
[145]
Young Gil Park and Benjamin Goldberg. Escape analysis on lists. In PLDI [148], pages 116-127.
Key: Park-Goldberg:1992.
[146]
Proceedings of the ACM SIGPLAN '88 Conference on Programming Language Design and Implementation (PLDI), volume 27(3) of SIGPLAN Notices, Atlanta, Georgia, June 1988. ACM Press.
Key: PLDI:88.
[147]
Proceedings of the ACM SIGPLAN '89 Conference on Programming Language Design and Implementation (PLDI), volume 24(7) of SIGPLAN Notices, Portland, Oregon, June 1989. ACM Press.
Key: PLDI:89.
[148]
Proceedings of the ACM SIGPLAN '92 Conference on Programming Language Design and Implementation (PLDI), volume 27(6) of SIGPLAN Notices, San Francisco, California, July 1992. ACM Press.
Key: PLDI:92.
[149]
Proceedings of the ACM SIGPLAN '93 Conference on Programming Language Design and Implementation (PLDI), volume 28(6) of SIGPLAN Notices, Albuquerque, New Mexico, June 1993. ACM Press.
Key: PLDI:93.
[150]
Proceedings of the ACM SIGPLAN '94 Conference on Programming Language Design and Implementation (PLDI), volume 29(6) of SIGPLAN Notices, Orlando, Florida, June 1994. ACM Press.
Key: PLDI:94.
[151]
Proceedings of the ACM SIGPLAN '95 Conference on Programming Language Design and Implementation (PLDI), volume 30(6) of SIGPLAN Notices, La Jolla, California, June 1995. ACM Press.
Key: PLDI:95.
[152]
Proceedings of the ACM SIGPLAN '97 Conference on Programming Language Design and Implementation (PLDI), volume 32(5) of SIGPLAN Notices, Las Vegas, Nevada, June 1997. ACM Press.
Key: PLDI:97.
[153]
Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation (PLDI), volume 33(5) of SIGPLAN Notices, Montreal, Canada, June 1998. ACM Press.
Key: PLDI:98.
[154]
Proceedings of the ACM SIGPLAN '2000 Conference on Programming Language Design and Implementation (PLDI), volume 35(5) of SIGPLAN Notices, Vancouver, Canada, June 2000. ACM Press.
Key: PLDI:2000.
[155]
Proceedings of the ACM SIGPLAN '2001 Conference on Programming Language Design and Implementation (PLDI), volume 36(5) of SIGPLAN Notices, Vancouver, Canada, May 2001. ACM Press.
Key: PLDI:2001.
[156]
Gordon Plotkin, Colin Stirling, and Mads Tofte, editors. Proof, Language, and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000.
Key: MILNER:2000.
[157]
Proceedings of the Second Annual ACM Symposium on Principles of Programming Languages (POPL), Palo Alto, California, January 1975. ACM Press.
Key: POPL:75.
[158]
Proceedings of the Fifth Annual ACM Symposium on Principles of Programming Languages (POPL), Tucson, Arizona, January 1978. ACM Press.
Key: POPL:78.
[159]
Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, January 1988. ACM Press.
Key: POPL:88.
[160]
Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, January 1990. ACM Press.
Key: POPL:90.
[161]
Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, January 1991. ACM Press.
Key: POPL:91.
[162]
Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages (POPL), Charleston, South Carolina, January 1993. ACM Press.
Key: POPL:93.
[163]
Proceedings of the Twenty-first Annual ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, January 1994. ACM Press.
Key: POPL:94.
[164]
Proceedings of the Twenty-third Annual ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, January 1996. ACM Press.
Key: POPL:96.
[165]
Proceedings of the Twenty-fourth Annual ACM Symposium on Principles of Programming Languages (POPL), Paris, France, January 1997. ACM Press.
Key: POPL:97.
[166]
Proceedings of the Twenty-sixth Annual ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, January 1999. ACM Press.
Key: POPL:99.
[167]
Proceedings of the Twenty-seventh Annual ACM Symposium on Principles of Programming Languages (POPL), Boston, Massachusetts, January 2000. ACM Press.
Key: POPL:2000.
[168]
Proceedings of the Twenty-eighth Annual ACM Symposium on Principles of Programming Languages (POPL), London, UK, January 2001. ACM Press.
Key: POPL:2001.
[169]
Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), Montreal, Canada, September 2000. ACM Press.
Key: PPDP:2000.
[170]
Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), Firenze, Italy, September 2001. ACM Press.
Key: PPDP:2001.
[171]
David J. Pym. On bunched predicate logic. In LICS [116], pages 183-192.
* Key: Pym:1999.
[172]
David J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. 2000. Draft of a forthcoming research monograph.
Key: Pym-book:2000.
[173]
Jakob Rehof and Manuel Fähndrich. Type-based flow analysis: From polymorphic subtyping to cfl-reachability. In POPL [168], pages 54-66.
Key: Rehof-Faehndrich:2001.
[174]
John C. Reynolds. Syntactic control of interference. In POPL [158], pages 39-46. Reprinted in cite [vol. 1, pages 273-286]OHearn-Tennent:1997.
Key: Reynolds:1978.
[175]
John C. Reynolds. Syntactic control of interference, part 2. In Ausiello et al. [4], pages 704-722.
Key: Reynolds:1989.
[176]
John C. Reynolds. Intuitionistic reasoning about shared mutable data structures. In Jim Davies [94].
* Key: Reynolds:2000.
[177]
Douglas T. Ross. The AED free storage package. Communications of the ACM, 10(8):481-492, 1967.
* Key: Ross:1967.
[178]
Cristina Ruggieri and Thomas P. Murtagh. Lifetime analysis of dynamically allocated objects. In POPL [159], pages 285-293.
Key: Ruggieri-Murtagh:1988.
[179]
Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 20(1):1-50, 1998.
Key: Sagiv-Reps-Wilhelm:1998.
[180]
Jacob T. Schwartz. Optimization of very high level languages --- I: Value transmission and its corollaries. Computer Languages, 1(2):161-194, 1975.
Key: Schwartz:1975a.
[181]
Jacob T. Schwartz. Optimization of very high level languages --- II: Deducing relationships of inclusion and membership. Computer Languages, 1(3):197-218, 1975.
Key: Schwartz:1975b.
[182]
Jacob T. Schwartz. Optimization of very high level languages (parts I and II). Computer Languages, 1(2 & 3):161-194, 197-218, 1975.
Key: Schwartz:1975.
[183]
Miley Semmelroth and Amr Sabry. Monadic encapsulation in ML. In ICFP [86], pages 8-17.
Key: Semmelroth-Sabry:1999.
[184]
Frederick Smith, David Walker, and Greg Morrisett. Alias types. In Smolka [185], pages 366-381.
Key: Smith-Walker-Morrisett:2000.
[185]
Gert Smolka, editor. Proceedings of the Ninth European Symposium on Programming (ESOP), number 1782 in Lecture Notes in Computer Science, Berlin, Germany, March 2000. Springer-Verlag.
Key: ESOP:2000.
[186]
Bjarne Steensgaard. Points-to analysis by type inference of programs with structures and unions. In Gyimóthy [64], pages 136-150.
Key: Steensgaard:1996b.
[187]
Bjarne Steensgaard. Points-to analysis in almost linear time. In POPL [164], pages 32-41.
Key: Steensgaard:1996a.
[188]
Proceedings of the Seventh ACM Symposium on Theory of Computing (STOC), Albuquerque, New Mexico, May 1975. ACM Press.
Key: STOC:75.
[189]
David Stoutamire. Portable, Modular Expression of Locality. PhD thesis, University of California at Berkeley, 1997.
Key: Stoutamire:1997.
[190]
Joseph E. Stoy, editor. Proceedings of the Fourth International Conference on Functional Programming and Computer Architecture (FPCA), London, England, September 1989. ACM Press.
Key: FPCA:89.
[191]
Robert E. Strom and Daniel M. Yellin. Extending typestate checking using conditional liveness analysis. IEEE Transactions on Software Engineering, 19(5):478-485, May 1993.
Key: Strom-Yellin:1993.
[192]
Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12(1):157-171, January 1986.
Key: Strom-Yemini:1986.
[193]
S. Doaitse Swierstra, editor. Proceedings of the Eigth European Symposium on Programming (ESOP), number 1576 in Lecture Notes in Computer Science, Amsterdam, The Netherlands, February 1999. Springer-Verlag.
Key: ESOP:99.
[194]
Jean-Pierre Talpin. Theoretical and Practical Aspects of Type and Effect Inference. PhD thesis, Ecole des Mines de Paris, 1993. French title: Aspects théoriques et pratiques de l'Inférence de types et d'effets.
* Key: Talpin:1993.
[195]
Jean-Pierre Talpin. A simplified account of region inference. Technical Report RR-4104, INRIA, Rennes, France, 2001.
* Key: Talpin:2001.
[196]
Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region, and effect inference. Journal of Functional Programming, 2(3):245-271, 1992.
* Key: Talpin-Jouvelot:1992.
[197]
Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. In LICS [115], pages 162-173. An extended version appeared as [198].
Key: Talpin-Jouvelot:1992b.
[198]
Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information & Computation, 111(2):245-296, 1994.
* Key: Talpin-Jouvelot:1994.
[199]
Yan-Mei Tang and Pierre Jouvelot. Control-flow effects for escape analysis. In WSA [228], pages 313-321.
Key: Tang-Jouvelot:1992.
[200]
Mads Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Edinburgh University, Department of Computer Science, Edinburgh University, 1988.
Key: Tofte:1988.
[201]
Mads Tofte. Storage mode analysis, 1994. Preliminary report on the storage mode analysis in the ML Kit. See [16] for details.
Key: Tofte:1994.
[202]
Mads Tofte. A brief introduction to regions. In Jones [97], pages 186-195.
* Key: Tofte:1998.
[203]
Mads Tofte and Lars Birkedal. A region inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):724-767, 1998.
* Key: Tofte-Birkedal:1998.
[204]
Mads Tofte and Lars Birkedal. Unification and polymorphism in region inference. In Plotkin et al. [156], pages 389-423.
* Key: Tofte-Birkedal:2000.
[205]
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Højfeld Olesen, Peter Sestoft, and Peter Bertelsen. Programming with regions in the ML Kit. Technical Report DIKU-TR-97/12, Department of Computer Science, University of Copenhagen (DIKU), 1997.
* Key: Tofte-al:1997.
[206]
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Højfeld Olesen, Peter Sestoft, and Peter Bertelsen. Programming with regions in the ML Kit (for version 3). Technical Report DIKU-TR-98/25, Department of Computer Science, University of Copenhagen (DIKU), 1998. An earlier version, version 2, of the ML Kit is described in [205].
* Key: Tofte-al:1998.
[207]
Mads Tofte and Niels Hallenberg. Region-based memory management in perspective. In Henglein et al. [73], pages 23-30.
Key: Tofte-Hallenberg:2001.
[208]
Mads Tofte and Jean-Pierre Talpin. Data region inference for polymorphic functional languages (technical summary). Technical Report EMP/CRI/A-229, Ecole des Mines de Paris, 1992.
Key: Tofte-Talpin:1992.
[209]
Mads Tofte and Jean-Pierre Talpin. A theory of stack allocation in polymorphically typed languages. Technical Report DIKU-TR-93/15, Department of Computer Science, University of Copenhagen (DIKU), 1993. Extended version of [210].
* Key: Tofte-Talpin:1993.
[210]
Mads Tofte and Jean-Pierre Talpin. Implementing the call-by-value lambda-calculus using a stack of regions. In POPL [163], pages 188-201. An extended version appeared as [209].
* Key: Tofte-Talpin:1994.
[211]
Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information & Computation, 132(2):109-176, 1997.
* Key: Tofte-Talpin:1997.
[212]
David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In FPCA [50], pages 1-11.
Key: Turner-Wadler-Mossin:1995.
[213]
Magnus Vejlstrup. Multiplicity inference. Master's thesis, Department of Computer Science, University of Copenhagen (DIKU), September 1994.
* Key: Vejlstrup:1994.
[214]
Per Velschow and Morten Voetmann Christensen. Region-based memory management in Java. Master's thesis, Department of Computer Science, University of Copenhagen (DIKU), 1998.
* Key: Velschow-Voetmann:1998.
[215]
Kiem-Phong Vo. Vmalloc: A general and efficient memory allocator. Software--Practice and Experience, 26(3):357-374, 1996.
* Key: Vo:1996.
[216]
Philip Wadler. The marriage of effects and monads. In ICFP [85], pages 63-74.
Key: Wadler:1998.
[217]
David Walker, Karl Crary, and Greg Morrisett. Typed memory management via static capabilities. ACM Transactions on Programming Languages and Systems, 22(4):701-771, July 2000.
Key: Walker-Crary-Morrisett:2000.
[218]
David Walker and Greg Morrisett. Alias types for recursive data structures. In Crary [32], page ??
Key: Walker-Morrisett:2000.
[219]
Mitchell Wand and Dino P. Oliva. Proving the correctness of storage representations. In LFP [113], pages 151-160.
Key: Wand-Oliva:1992.
[220]
Daniel C. Wang and Andrew W. Appel. Type-preserving garbage collectors. In POPL [168], pages 166-178.
Key: Wang-Appel:2001.
[221]
David A. Watt, editor. Proceedings of the Ninth International Conference on Compiler Construction (CC), volume 1781 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
Key: CC:2000.
[222]
Reinhard Wilhelm, Mooly Sagiv, and Thomas Reps. Shape analysis. In Watt [221], pages 1-17.
Key: Wilhelm-Sagiv-Reps:2000.
[223]
Paul R. Wilson. Uniprocessor garbage collection techniques. In Bekkers and Cohen [12], pages 1-42. Extended version in [224].
Key: Wilson:1992.
[224]
Paul R. Wilson. Uniprocessor garbage collection techniques. Expanded version of [223]; to appear in ACM Computing Surveys, 1995.
Key: Wilson:1995.
[225]
Paul R. Wilson, Mark S. Johnstone, Michael Neely, and David Boles. Dynamic storage allocation: A survey and critical review. In Baker [8], pages 1-116.
Key: Wilson-al:1995.
[226]
Andrew K. Wright. Typing references by effect inference. In Krieg-Brückner [106], pages 473-491.
Key: Wright:1992.
[227]
Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information & Computation, 115(1):38-94, 1994.
Key: Wright-Felleisen:1994.
[228]
Proceedings of the Workshop on Static Analysis (WSA) '92, Bordeaux, France, September 1992. IRISA.
Key: WSA:92.
[229]
Silvano dal Zilio and Andrew D. Gordon. Region analysis and a pi -calculus with groups. In Nielsen and Rovan [134], pages 1-20.
* Key: Zilio-Gordon:2000.

[ valid XHTML and CSS ]