Abstract: Is it possible to prove the deletion of a computer program? While this task is clearly impossible using classical information alone, the laws of quantum mechanics may admit a solution to this conundrum. In this work, we propose a new approach to answer this question, using quantum information. We put forward the notion of obfuscation with certified deletion as the cornerstone of our framework. We propose a new security definition for this primitive, and we show a construction that satisfies it, assuming the existence of post-quantum one-way functions and post-quantum indistinguishability obfuscation. Our definition naturally implies two different notions of functional encryption with certified deletion: one with secret key deletability and another with ciphertext deletability. Additionally, it naturally gives a positive result for a form of program copy-protection called secure software leasing. In fact, we are able to achieve a strong notion of secure software leasing where even a dishonest evaluator cannot evaluate the program after returning it.