Oris teme
-
-
Eden boljših učbenikov za teorijo programskih jezikov. Par izvodov je na voljo tudi v knjižnici.
-
- 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.
-
- podatkovni tipi
- funkcije
- miksfiksna notacija
- luknje
- interaktivno pisanje programov
- moduli
- odvisni tipi
-
Učbenik za teorijo programskih jezikov, v celoti napisan v Agdi
-
- 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.
-
- operacijska semantika
- statično preverjanje pravilnosti
- izrek o varnosti
-
- sintaksa
- substitucija
- operacijska semantika malih korakov
- Churchevo kodiranje
-
Prikaz, kako samo s spremenljivkami, abstrakcijo in aplikacijo predstavimo naravna števila, logične vrednosti, pare, sezname, …
-
- sistem tipov za λ-račun
- lema o substituciji
- izrek o varnosti (napredek in ohranitev)
- Barendregtova kocka
-
- 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
-
- ločitev izrazov na vrednosti in izračune (fine-grain call-by-value)
- izjeme
- nedeterminizem
- pomnilnik
-
- deBruijnovi indeksi
- intrinzični tipi
- izrek o varnosti
-
- naivna denotacijska semantika
- zdravost denotacijske semantike
- rekurzivne definicije so fiksne točke
-
- 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
-
- monade
- primeri monad
- proste algebre
- algebrajske operacije in drevesa izvajanj
-
- 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