Pri predmetu spoznamo koncepte in principe, na katerih slonijo moderni programski jeziki. Poudarek je na razumevanju s stališča programerja, čeprav se posvetimo tudi teoretičnim osnovam, na katerih sloni načrtovanje programskih jezikov.
1. Uvod in artimetični izrazi
- o programskih jezikih na splošno
- anatomija programskega jezika
- prvi primer: aritmetični izrazi s spremenljivkami
2. Ukazni programski jezik
- spremenljivke in aritmetika
- boolove vrednosti
- osnovne kontrolne strukture (zanke in pogojni stavek)
- operacijska semantika ukaznega jezika
- denotacijska semantika
- ekvivalenca programov
3. Dokazovanje pravilnosti programov
- dokazovanje pravilnosti za ukazni jezik (Hoare-style)
- pravilnost programa glede na dano specifikacijo
- Delna pravilnost `{P} c {Q}` in popolna pravilnost `[P] c [Q]`
- Pravila za dokazovanje: splošna pravila, invarianta zanke, dokazovanje popolne pravilnosti
4. Lambda račun
- zapis funkcij s funkcijskim predpisom:
- vezane in proste spremenljivke
- računsko pravilo (β-redukcija) za funkcijski predpis
- λ-račun brez tipov
- evaluacijske strategije (neučakana, lena)
- konfluentnost λ-računa
- primeri programov v λ-računu
5. Deklarativno programiranje in algebrajski tipi
- deklarativno programiranje
- algebrajski tipi:
- konstruktorji in destruktorji
- primeri deklarativnih jezikov: Haskell, ML, Racket
6. Rekurzivni tipi in rekurzija
- rekurzivni tipi, primeri
- rekurzivne definicije
- rekurzija kot negibna točka
- leno in neučakano računanje
- induktivni tipi – strukturna indukcija
- koinduktivni tipi
7. Polimorfizem in izpeljava tipov
- polimorfni tipi
- parametrični polimorfizem, najsplošnejši tip
- ad-hoc polimorfizem
- generično programiranje
- izpeljava tipov
8. Abstrakcija
- specifikacija/vmesnik in implementacija/modul
- abstrakcija implementacije, abstraktni tipi
- funktorji: preslikave iz implementacije v implementacijo
- primeri v OCaml, Javi in Haskellu
9. Logično programiranje
- pravila sklepanja kot program
- izvajanje programa je iskanje dokaza
- kako deluje prolog, zruževanje in meta-spremenljivke
- programiranje z omejitvami
10. Zapisi in objekti
- zapisi in tipi zapisov
- strukturni podtipi
- objekti kot rekurzivni zapisi
- objekti kot "encapsulated state" in metode kot "message passing"
- razredi
