A tantárgy az alábbi témakörök ismeretére épít:
Javasolt ismeretek: 1. valamilyen legalább polimorf típusrendszert, függvénytípust vagy pattern matchinget használó programnyelv alapszintű ismerete (pl.: C++, Python, Type/JavaScript, Wolfram nyelv), 2. lineáris algebra elméleti háttere alapszinten.
A tantárgy szerepe a képzés céljának megvalósításában:
Szabadon választható tantárgy
A tantárgy részletes tematikája magyarul és angolul:
1. A típuselmélet, mint a matematika alapja. 2. Induktív konstrukciók kalkulusa (természetes számok, listák, fák). 3. Curry--Howard-izomorfizmus: logika mint programozási nyelv. 4. Prop adattípus. 5. Első rendű logika. 6. Kartéziusi kategóriák. 7. Kartéziusian zárt kategóriák. 8. Reprezentálható funktorok. 9. Yoneda-tételkör. 10. Algebrai adattípusok. 11. Monádok. 12. Mellékhatások kezelése monádokkal. 13. Kontinuációk.
In English
1. Type Theory as a Foundation for Mathematics. 2. Calculus of Inductive Constructions (naturals, lists, trees). 3. Curry-Howard Isomorphism: Logic as Programming Language. 4. Prop Data Type. 5. First-Order Logic. 6. Cartesian Categories. 7. Cartesian Closed Categories. 8. Representable Functors. 9. Yoneda Lemma. 10. Algebraic Data Types. 11. Monads. 12. Handling Side Effects with Monads. 13. Continuations.
Követelmények szorgalmi időszakban:
Egy zárthelyi dolgozat az előadás anyagából a félév közepén, és egy beadandó programozási feladatsor bizonyításasszisztensben elkészítve (pl. Lean, Rocq, Agda) a gyakorlaton tanultak alapján.
Követelmények vizsgaidőszakban:
Konzultációs lehetőségek:
Jegyzet, tankönyv, felhasználható irodalom:
Barr, M., & Wells, C. (1999). Category Theory Lecture Notes for ESSLLI. Retrieved from https://fldit-www.cs.tu-dortmund.de/~peter/barrwells.pdf
Thompson, S. (1999). Type Theory & Functional Programming. (Computing Laboratory, University of Kent). Retrieved from https://kar.kent.ac.uk/20998/1/ttfp.pdf
Milewski, B. (2019). Category Theory for Programmers. Independently published. Available at: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Nyomtatóbarát változat
