Topic outline
- Eden boljših učbenikov za teorijo programskih jezikov. Par izvodov je na voljo tudi v knjižnici.
Praksa programskih jezikov
- sintaksa in semantika
- konkretna in abstraktna sintaksa
- BNF sintaksa
- programski jezik IMP
- ponovitev osnov funkcijskega programiranja
- izvajanje
- statično preverjanje
- razčlenjevalniki (parserji)
- Članek o Backus-Naurjevi obliki in njenih razširitvah.
Zbirka dokumentiranih implementacij majhnih programskih jezikov.
Zbirka člankov, v katerih je razloženo, kako iz majhnih parserjev sestavljamo velike. Programi so sicer napisani v jeziku F#, ki pa je precej podoben OCamlu.
Uvod v Agdo
- podatkovni tipi
- funkcije
- miksfiksna notacija
- luknje
- interaktivno pisanje programov
- moduli
- odvisni tipi
- Učbenik za teorijo programskih jezikov, v celoti napisan v Agdi
Indukcija
- primeri induktivno definiranih množic
- konstrukcija induktivno definiranih množic
- induktivno definirane relacije
- dokazovanje z indukcijo
Gradiva pri predmetu Part IA Discrete Mathematics na univerzi v Cambridgeu. Strani 12–23 natančno razložijo induktivne definicije in dokaze z indukcijo.
Metateorija programskih jezikov
- operacijska semantika
- statično preverjanje pravilnosti
- izrek o varnosti
λ-račun
- sintaksa
- substitucija
- operacijska semantika malih korakov
- Churchevo kodiranje
Prikaz, kako samo s spremenljivkami, abstrakcijo in aplikacijo predstavimo naravna števila, logične vrednosti, pare, sezname, …
Tipi
- sistem tipov za λ-račun
- lema o substituciji
- izrek o varnosti (napredek in ohranitev)
- Barendregtova kocka
Izpeljava tipov
- Hindley-Milnerjev algoritem
- izpeljava tipa izraza in nastavitev sistema enačb med tipi
- iskanje najsplošnejše rešitve sistema enačb
- zdravost in polnost izpeljanih tipov
- implementacija Hindley-Milnerjevega algoritma
Računski učinki
- ločitev izrazov na vrednosti in izračune (fine-grain call-by-value)
- izjeme
- nedeterminizem
- pomnilnik
Mehanizacija dokazov
- deBruijnovi indeksi
- intrinzični tipi
- izrek o varnosti
Denotacijska semantika
- naivna denotacijska semantika
- zdravost denotacijske semantike
- rekurzivne definicije so fiksne točke
Domene
- domene in zvezne preslikave
- izrek o obstoju najmanjše fiksne točke
- interpretacije tipov so domene, interpretacije izrazov so zvezne preslikave
- kontekstna ekvivalenca
- zadostnost denotacijske semantike
- izrazi z isto interpretacijo so navzven ekvivalentni
- This topic
Monade in algebrajski učinki
- monade
- primeri monad
- proste algebre
- algebrajske operacije in drevesa izvajanj
Prestrezniki učinkov
- homomorfizmi algeber
- prestrezniki izjem in učinkov
- prestrezniki za izpis, nedeterminizem in naključje
- Teoretični uvod v matematično ozadje algebrajskih učinkov
- Domača stran prototipnega programskega jezika Eff
- Teoretični uvod v programsko ozadje algebrajskih učinkov
- Raziskovalni članek, ki je uvedel praktično programiranje s prestrezniki - primeri so v razdelku 6
Poglavje 2.4 dokaže in razloži pomembne lastnosti teorije za state
Zanimivosti in dodatna literatura