D. Aspinall and M. Hofmann, Another Type System for In-Place Update, Proceedings of the 11th European Sysmposium on Programming, ESOP'02, pp.36-52, 2002.
DOI : 10.1007/3-540-45927-8_4

D. Aspinall, M. Hofmann, and M. Kone?n´kone?n´y, A type system with usage aspects, Journal of Functional Programming, vol.7, issue.02, pp.141-178, 2008.
DOI : 10.1016/0304-3975(93)90110-F

G. Barthe, B. Grégoire, C. Kunz, and T. Rezk, Certificate translation for optimizing compilers, SAS'06, pp.301-317, 2006.
DOI : 10.1145/1538917.1538919

L. Beringer, M. Hofmann, A. Momigliano, and O. Shkaravska, Automatic Certification of Heap Consumption, LPAR'04, LNAI 3452, pp.347-362, 2005.
DOI : 10.1007/978-3-540-32275-7_23

R. Bornat, Proving Pointer Programs in Hoare Logic, Proc. 5th Int. Conf. Mathematics of Program Construction, MPC'00, pp.102-126, 2000.
DOI : 10.1007/10722010_8

J. De-dios and R. Peña, A Certified Implementation on Top of the Java Virtual Machine, Formal Method in Industrial Critical Systems, FMICS'09, pp.181-196, 2009.
DOI : 10.1007/978-3-642-04570-7_14

J. De-dios and R. Peña, Formal Certification of a Resource-Aware Language Implementation, Int. Conf. on Theorem Proving in Higher Order Logics, TPHOL'09, pp.196-211, 2009.
DOI : 10.1007/3-540-45620-1_5

M. Hofmann and S. Jost, Static prediction of heap space usage for first-order functional programs, Proc. 30th ACM Symp. on Principles of Programming Languages, POPL'03, pp.185-197, 2003.

D. C. Luckham and N. Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.226-244, 1979.
DOI : 10.1145/357073.357078

F. Mehta and T. Nipkow, Proving Pointer Programs in Higher-Order Logic, Automated Deduction CADE-19, pp.121-135, 2003.

M. Montenegro, R. Peña, and C. Segura, A type system for safe memory management and its proof of correctness, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.152-162, 2008.
DOI : 10.1145/1389449.1389468

M. Montenegro, R. Peña, and C. Segura, An Inference Algorithm for Guaranteeing Safe Destruction, Selected papers of Logic-Based Program Synthesis and Transformation, LOPSTR'08, pp.135-151, 2009.
DOI : 10.1006/inco.1996.2613

M. Montenegro, R. Peña, and C. Segura, A Simple Region Inference Algorithm for a First-Order Functional Language, Work. on Functional and Logic Programming, pp.145-161, 2009.
DOI : 10.1007/978-3-642-11999-6_10

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

G. C. Necula and P. Lee, Safe Kernel Extensions Without Run-Time Checking, Proceedings of the Second Symposium on Operating Systems Design and Implementation, pp.229-243, 1996.
DOI : 10.1145/238721.238781
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.6054