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