Abstract
Safe is a first-order eager functional language with destructive pattern matching controlled by the programmer. A previously presented type system is used to avoid dangling pointers arising from the inadequate usage of this facility. In this paper we present a type inference algorithm, prove its correctness w.r.t. the type system, describe its implementation and give a number of successfully typed examples.
Work supported by the projects TIN2008-06622-C03-01/TIN (STAMP), S-0505/TIC/0407 (PROMESAS) and the MEC FPU grant AP2006-02154.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aiken, A., Fähndrich, M., Levien, R.: Better Static Memory Management: Improving Region-based Analysis of Higher-order Languages. In: PLDI 1995, pp. 174–185. ACM, New York (1995)
Aspinall, D., Hofmann, M., Konečný, M.: A Type System with Usage Aspects. Journal of Functional Programming 18(2), 141–178 (2008)
Birkedal, L., Tofte, M., Vejlstrup, M.: From Region Inference to von Neumann Machines via Region Representation Inference. In: POPL 1996, pp. 171–183. ACM, New York (1996)
Henglein, F., Makholm, H., Niss, H.: A Direct Approach to Control-flow Sensitive Region-based Memory Management. In: PPDP 2001, pp. 175–186. ACM, New York (2001)
Hofmann, M., Jost, S.: Static Prediction of Heap Space Usage for First-order Functional Programs. In: POPL 2003, pp. 185–197. ACM, New York (2003)
Hudak, P.: A Semantic Model of Reference Counting and its Abstraction. In: Lisp and Functional Programming Conference, pp. 351–363. ACM Press, New York (1986)
Inoue, K., Seki, H., Yagi, H.: Analysis of Functional Programs to Detect Run-Time Garbage Cells. ACM TOPLAS 10(4), 555–578 (1988)
Jones, S.B., Le Metayer, D.: Compile Time Garbage Collection by Sharing Analysis. In: FPCA 1989, pp. 54–74. ACM Press, New York (1989)
Kobayashi, N.: Quasi-linear Types. In: POPL 1999, pp. 29–42. ACM Press, New York (1999)
Montenegro, M., Peña, R., Segura, C.: A Simple Region Inference Algorithm for a First-Order Functional Language. In: TFP 2008, pp. 194–208 (2008)
Montenegro, M., Peña, R., Segura, C.: A Type System for Safe Memory Management and its Proof of Correctness. In: PPDP 2008, pp. 152–162. ACM, New York (2008)
Montenegro, M., Peña, R., Segura, C.: An Inference Algorithm for Guaranteeing Safe Destruction (extended version). Technical report, SIC-8-08. UCM (2008), http://federwin.sip.ucm.es/sic/investigacion/publicaciones/pdfs/SIC-8-08.pdf
Odersky, M.: Observers for Linear Types. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 390–407. Springer, Heidelberg (1992)
Peña, R., Segura, C.: Formally Deriving a Compiler for SAFE. In: Horváth, Z., Zsók, V. (eds.) Preliminary proceedings of IFL 2006, pp. 429–426. Technical Report, 2006-S01. Eötvös Loránd University (2006)
Peña, R., Segura, C., Montenegro, M.: A Sharing Analysis for Safe. In: Trends in Functional Programming, vol. 7, pp. 109–128 (2007)
Tofte, M., Birkedal, L., Elsman, M., Hallenberg, N., Olesen, T.H., Sestoft, P.: Programming with regions in the MLKit (revised for version 4.3.0). Technical report, IT University of Copenhagen, Denmark (2006)
Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
Wadler, P.: Linear types can change the world! In: IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 561–581. North-Holland, Amsterdam (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Montenegro, M., Peña, R., Segura, C. (2009). An Inference Algorithm for Guaranteeing Safe Destruction . In: Hanus, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2008. Lecture Notes in Computer Science, vol 5438. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00515-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-00515-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00514-5
Online ISBN: 978-3-642-00515-2
eBook Packages: Computer ScienceComputer Science (R0)