A Certified Implementation on Top of the Java Virtual Machine. - Javier de Dios; Ricardo Peña-Marí (FMICS, 2009)

Formal Certification of a Resource-Aware Language Implementation. - Javier de Dios; Ricardo Peña-Marí (TPHOLs, 2009)

Certified Absence of Dangling Pointers in a Language with Explicit Deallocation. - Javier de Dios; Manuel Montenegro; Ricardo Peña (IFM, 2010)

Certification of Safe Polynomial Memory Bounds. - Javier de Dios; Ricardo Peña (FM, 2011)