Eksplicitna izpeljava učinkovKoprivec, Filip (Avtor) Pretnar, Matija (Mentor) algebrajski učinki in njihovi prestreznikiizpeljava tipoveksplicitni tipiV delu je predstavljena avtomatska izpeljava in eksplicitna dopolnitev tipov programov z algebrajskimi učinki. Predstavljen je MiniEff, preprost funkcijski programski jezik s polimorfnimi shemami in podporo za algebrajske učinke, ki temelji na jeziku Eff. Za MiniEff sta podana in dokazana izrek o napredku in izrek o ohranitvi. Predstavljen in podan je jezik ImpEff, ki tipom v jeziku MiniEff doda informacije o sproženih učinkov, skupaj s pripadajočim sistemom tipov, ki uporablja podtipe. Izreka o napredku in ohranitvi sta posodobljena in dokazana tudi za ImpEff, kjer so pojasnjene ključne spremembe glede na jezik MiniEff. Podan je jezik ExEff, ki predstavlja eksplicitno obliko jezika ImpEff, osnovano na polimorfnem lambda računu. Podan je sistem tipov in izrekoma o napredku in ohranitvi in pripadajočima dokazoma. Podana so pravila za dopolnitev programov iz jezika ImpEff v jezik ExEff skupaj z dokazom, da dopolnitev ohranja tipe. Prikazana je variacija Hindley-Milnerjevega algoritma za izpeljavo tipov, ki programom iz jezika ImpEff določi tipe in jih dopolni v eksplicitno obliko v jeziku ExEff. Za prikazani algoritem sta podana izreka o zdravosti in polnosti. Prikazana je sprememba relacije izpeljave in dopolnitve z uporabo lenih substitucij, ki je trenutno uporabljana v prevajalniku za jezik Eff.20192019-09-14 07:16:00Magistrsko delo/naloga110366sl