The Safe Project

Safe is a first-order eager functional language with facilities for programmer-controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap where the compiler allocates data structures.

Most functional languages abstract the programmer from the memory management. Should the memory be exhausted, the garbage collector will copy/mark the live part of the heap and will consider the rest as free. This normally implies the suspension of program execution for some time. Occasionally, not enough free memory has been recovered and the program simply aborts.

In some contexts, this scheme may not be acceptable. Safe does not use a garbage collector and is equipped with a set of compile-time analyses aimed at inferring an upper bound on memory consumption. Additionally the compiler (will hopefully) provide a formal certificate proving this property.

The Safe project has been funded by the Spanish grants TIN2004-07943-C04-04 (SELF), S-0505/TIC/0407 (PROMESAS), and is currently funded by the grant TIN2008-06622-C03-01 (STAMP).

• You can download a file with some Safe examples
• You can find more details, examples, and download the compiler at our page (for linux platforms)

Refereed publications (since 2006 up to now)

• J. de Dios, R. Peña
  "Certification of Safe Polynomial Memory Bounds"
  17th Int. Symp. on Formal Methods, FM'11, Limerick (Ireland), June 2011, LNCS (to appear), pages 1-15
  .pdf


• J. de Dios, M. Montenegro, R. Peña
  "Certified Absence of Dangling Pointers in a Language with Explicit Deallocation"
  8th Int. Conf. on Integrated Formal Methods, IFM 2010, Nancy (France), LNCS 6396, pp. 305-319
  .pdf


• M. Montenegro, R. Peña, C. Segura
  "A Space Consumption Analysis By Abstract Interpretation"
  Selected papers of Workshop on Foundational and Practical Aspects of Resource Analysis, FOPARA'09, Eindhoven (The Netherlands), Nov. 2009, LNCS 6324, Springer, pages 34-50.
  .pdf


• M. Montenegro, R. Peña, C. Segura
  "Experiences in Developing a Compiler for Safe using Haskell"
  Proceedings of Taller de Programación Funcional, TPF'09, San Sebastián (Spain), Sept. 2009, pages 31-38
  .pdf


• J. de Dios, R. Peña
  "Formal Certification of a Resource-Aware Language Implementation"
  Proceedings of Int. Conf. on Theorem Proving in Higher Order Logics, TPHOL'09, Munich (Germany), Aug. 2009, LCNS 5674, Springer, pages 196-211
  .pdf


• J. de Dios, R. Peña
  "A Certified Implementation on top of the Java Virtual Machine"
  Proceedings of Formal Method in Industrial Critical Systems, FMICS'09, Eindhoven (The Netherlands), Nov. 2009, LCNS 5825, Springer, pages 181-196
  .pdf


• M. Montenegro, R. Peña, C. Segura
  "A Simple Region Inference Algorithm for a First-Order Functional Language"
  International Workshop on Functional and (Constraint) Logic Programming, WFLP 2009, , Brasilia (Brasil), June 2009, LNCS 5979, Springer, pages 145-161
  .pdf


• M. Montenegro, R. Peña, C. Segura
  "A Type System for Safe Memory Management and its Proof of Correctness"
  Proceedings of ACM Symposium on Principles and Practice of Declarative Programming, PPDP'08, Valencia (Spain), July 2008, ACM Press, pages 152-162.
  .pdf


• M. Montenegro, R. Peña, C. Segura
  "An Inference Algorithm for Guaranteeing Safe Destruction"
  Selected papers of Logic-Based Program Synthesis and Transformation, LOPSTR'08, Valencia (Spain), July 2008, LNCS 5438, Springer, pages 135-151
  .pdf


• M. Montenegro, R. Peña, C. Segura
  "A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation"
  Workshop on Functional and (Constraint) Logic Programming, WFLP'08, Siena, Italy July, 2008, ENTCS 246, 2009, pages 167-182
  .pdf


• S. Lucas, R. Peña
  "Rewriting Techniques for Analysing Termination and Complexity Bounds of SAFE Programs"
  Informal proceedings of Logic-Based Program Synthesis and Transformation, LOPSTR'08, Valencia, Spain, July 2008, pages 43-57
  .pdf


• R. Peña, C. Segura, M. Montenegro
  "A Sharing Analysis for SAFE"
  Selected Papers of Trends in Functional Programming, TFP'06, Intellect 2007, pages 109-128
  .pdf