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. Bizonyításkódok generálása AI segítségével. 4. Prop adattípus. AI hallucinációk kiszűrése és bizonyításvalidáció bizonyításasszisztens programcsomagokkal (pl. Agda, Rocq ill. Lean segítségével). 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. Generating proof code with the help of AI. 4. The Prop data type. Filtering out AI hallucinations and validating proofs with proof assistant software packages, such as Agda, Rocq, or Lean. 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, akár AI segítségével.
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
