Una transformación de doble negación (DNT) incrusta la lógica clásica en la lógica intuicionista. Tales traducciones corresponden a transformaciones de estilo de paso de continuación (CPS) en lenguajes de programación a través del isomorfismo de Curry-Howard. Una transformación selectiva de CPS utiliza un sistema de tipo y efecto para traducir selectivamente solo expresiones no triviales posiblemente con efectos computacionales en funciones CPS. En este documento, revisamos la transformación CPS convencional de llamada por valor (CBV) y su correspondiente DNT, y proporcionamos un enfoque lógico de una transformación selectiva de CPS de CBV definiendo un DNT selectivo a través del isomorfismo de Curry-Howard. Al utilizar un sistema de prueba anotado derivado del sistema de tipo y efecto correspondiente, nuestro DNT selectivo traduce pruebas clásicas en pruebas intuicionistas equivalentes, que son más pequeñas que las obtenidas por los DNT habituales. Creemos que nuestro trabajo puede servir como punto de referencia para estudios adicionales sobre el isomorfismo de Curry-Howard entre transformaciones CPS y DNTs.