Foundational Methods in Computer Science
Description
The relationship between computer science and mathematics stems directly from the work of Haskell Curry in the 1930’s and W.A. Howard and Per Martin-Lof in the 1960’s. In particular, the Curry-Howard correspondence establishes a direct relationship between computer programs and mathematical proofs. Mathematically, this relationship is best expressed using category theory, and can be done more succinctly as a direct correspondence between categories and programming languages. Category theorists, logicians and computer scientists have discussed their work and its implications to one another at FMCS meetings for more than 30 years. In recent years, connections between category theory and homotopy theory have been made apparent too.