The objective of the present work is to introduce the Curry-Howard isomorphism in depth to philosophers, computer scientists, programmers or any researcher who seeks to know the subject. Furthermore, through our research we seek to understand how the Curry-Howard isomorphism can help shape and answare philosophical questions about programming languages and thus demonstrate its philosophical significance.
The Curry-Howard isomorphism was first discovered by the logician-mathematician Haskell Curry when in 1934 he observed the similarity between some axioms of intuitionistic logic and combinatorial logic. This isomorphism is the observation that there is a given functional programming language corresponding to a given logic.
Despite the importance of the topic both for the Philosophy of Logic and for Computer Science, there are few works on the topic and most courses do not even address it. That's why we see the importance of this work that intends to introduce more people to the subject and thus expand the philosophical discussion about computing in Brazil.