O objetivo do presente trabalho é introduzir o isomorfismo Curry-Howard de maneira aprofundada para filósofos, cientistas da computação, programadores ou qualquer pesquisador que busque conhecer o tema. Além disso por meio da nossa pesquisa buscamos compreender como o isomorfismo Curry-Howard pode ajudar a moldar e resolver questões filosóficas sobre linguagens de programação e assim demonstrar sua significância filosófica.
O isomorfismo Curry-Howard foi descoberto pela primeira vez pelo lógico-matemático Haskell Curry quando em 1934 ele observou a similaridade entre alguns axiomas da lógica intuicionista e da lógica combinatória. Esse isomorfismo é a observação de que existe uma dada linguagem de programação funcional correspondente para uma dada lógica.
Apesar da importância do tema tanto para a Filosofia da Lógica quanto para a Ciência da Computação existem poucos trabalhos sobre o tema e a maioria dos cursos sequer o abordam. Por isso a vemos a importância deste trabalho que pretende introduzir mais pessoas no assunto e assim ampliar a discussão filosófica sobre a computação no Brasil.