MARCELO LEOPOLDO E SILVA DE CARVALHO FILHO

The goal of this work is to introduce the Curry-Howard isomorphism in depth to philosophers, computer scientists, programmers, or any researchers interested in exploring this subject. Furthermore, through our research, we aim to understand how the Curry-Howard isomorphism can help shape and address philosophical questions about programming languages, thereby demonstrating its philosophical significance. The Curry-Howard isomorphism was first discovered by the mathematical logician Haskell Curry in 1934 when he observed similarities between certain axioms of intuitionistic logic and combinatory logic. This isomorphism is the observation that there is a corresponding functional programming language for a given logic. Despite its importance for both the Philosophy of Logic and Computer Science, there are few works on this topic, and most academic courses do not even address it. Therefore, we see the importance of this work, which seeks to introduce more people to the subject and expand the philosophical discussion about computing in Brazil.