Budapesti Műszaki és Gazdaságtudományi Egyetem
Természettudományi Kar		 Tantárgy Adatlap
Tantárgy kód BMETEAGBsMTEFP-00
Tantárgy azonosító adatok
1. A tárgy címe Típuselmélet és funkcionális programozás
2. A tárgy angol címe Type Theory and Functional Programming
3. Heti óraszámok (ea + gy + lab) és a félévvégi követelmény típusa 2 + 1 + 0 v Kredit 4
4. Ajánlott/kötelező előtanulmányi rend
vagy Tantárgy kód 1 Rövid cím 1 Tantárgy kód 2 Rövid cím 2 Tantárgy kód 3 Rövid cím 3
4.1
4.2
4.3
5. Kizáró tantárgyak
6. A tantárgy felelős tanszéke Algebra és Geometria Tanszék
7. A tantárgy felelős oktatója Dr. Molnár Zoltán Gábor beosztása egyetemi adjunktus
Akkreditációs adatok
8. Akkreditációra benyújtás időpontja 2025.06.21. Akkreditációs bizottság döntési időpontja 2025.07.01.
Tematika
9. 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.
10. A tantárgy szerepe a képzés céljának megvalósításában (szak, kötelező, kötelezően választható, szabadon választható)
Szabadon választható tantárgy
11. A tárgy részletes tematikája

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.
12. Követelmények, az osztályzat (aláírás) kialakításának módja
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. vizsga-
időszakban		 Írásbeli vizsga
13. Pótlási lehetőségek
TVSZ szerint
14. Konzultációs lehetőségek
Az oktatóval egyeztetve
15. 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/
16. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka mennyisége órákban (a teljes szemeszterre számítva)
16.1 Kontakt óra
42
16.2 Félévközi felkészülés órákra
14
16.3 Felkészülés zárthelyire
14
16.4 Zárthelyik megírása
2
16.5 Házi feladat elkészítése
24
16.6 Kijelölt írásos tananyag elsajátítása (beszámoló)
0
16.7 Egyéb elfoglaltság
0
16.8 Vizsgafelkészülés
24
16.9 Összesen
120
17. Ellenőrző adat Kredit * 30
120
A tárgy tematikáját kidolgozta
18. Név beosztás Munkahely (tanszék, kutatóintézet, stb.)
Dr. Molnár Zoltán Gábor
egyetemi adjunktus
Algebra és Geometria Tanszék
A tanszékvezető
19. Neve aláírása
Dr. Hegedüs Pál