Abstract: In this master thesis we study category theory with special focus on Cartesian closed categories and simply typed \(\lambda-\)calculus. We describe the relationship between them, known as Curry-Howard-Lambek isomorphism. An introduction to the category theory and neccesary terms required for understanding the Curry-Howard-Lambek isomorphism are given. Programming language Haskell is used to demonstrate practical applications of category theory. We define Cartesian closed categories, type of category which has expressive power equivalent to the simply typed \(\lambda-\)calculus and demonstrate few examples of Cartesian closed categories. In the last chapter we define a construction that describes relationship between simply typed \(\lambda-\)calculus and Cartesian closed categories. Master thesis is finalized with an example which demonstrates interchangeability of functions in simply typed \(\lambda-\)caluclus with projections in Cartesian closed categories. A short overview with advantages of categorical approach to computation is given, demonstrating practicality with few well known programming libraries.
Publication Year: 2018
Publication Date: 2018-09-26
Language: en
Type: dissertation
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot