The Curry-Howard correspondence journey
Silvia Ghilezan (University of Novi Sad & Mathematical Institute SASA)
The Curry-Howard correspondence, also known as, the formulae-as-types and proofs-as-terms correspondence is a foundational concept that connects logic and computation. This correspondence establishes a deep connection between logical reasoning and computational processes. The origins of this idea can be traced back to the relationship between intuitionistic logic, lambda calculus, and combinatory logic. It has been extended to a wide range of different logical systems and formal calculi. Nowadays it is at the heart of formal verification of mathematical proofs. Its extension to various logical and computational frameworks highlights its versatility and broad applicability across different domains of computer science and mathematics. Due to this two-way correspondence the interplay between developments in logic and computation continues to shape both fields. We will give an overview from intuitionistic and classical logic along with the corresponding formal calculi to some recent advancements in the field.