Teorija programskih jezikov

Pogojev za vključitev v delo ni.

Pri predmetu se obravnava teorija programskih jezikov s poudarkom na uporabi matematičnih metod pri podajanju jezikov in analizi njihovih lastnosti. Obravnavajo se naslednje teme:
- konkretna in abstraktna sintaksa,
- induktivne definicije, definicije
- dokazovanje s strukturno indukcijo
- induktivni podatkovni tipi kot
- operacijska semantika kot
- funkcijski programski jeziki:
- polimorfizem, parametrični
- ukazni programski jeziki,
- denotacijska semantika: domene in
- izbirne vsebine: objektni leksična in gramatična analiza kot prevajanje konkretne v abstraktno sintakso podane z sodbami in pravili sklepanja po abstraktni sintaksi ali po strukturi izpeljave primer uporabe strukturnih definicij in strukturne indukcije induktivno definirana relacija, semantika malih in velikih korakov rekurzivne definicije, neučakani in leni jeziki, statična analiza, preverjanje tipov, varnost kot posledica leme o napredku in leme o ohranitvi, pomen varnosti v praksi polimorfizem in Hindley-Milnerjeva izpeljava tipov specifikacije in dokazovanje pravilnosti programov zvezne funkcije, izrek o obstoju negibnih točk, denotacijska semantika funkcijskega programskega jezika, interpretacija rekurzije z negibnimi točkami programski jeziki, paralelno računanje, logično programiranje.

1. R. M. Amadio, P.-L. Curien: Domains and lambda-calculi Cambridge : Cambridge University Press, cop. 1998.
2. B. C. Pierce: Types and programming languages, Cambridge (Mass.) : The MIT Press, cop. 200
3. J. C. Reynolds: Theories of programming languages, Cambridge : Cambridge University Press, 1998.

Cilj predmeta je predstavitev modernega, matematičnega pristopa, k teoriji programskih jezikov. Študenti pridobijo sposobnost analize programskih jezikov ter osnovnih konceptov povezanih z njimi.

Znanje in razumevanje:
Slušatelji se naučijo, kako načrtujemo in analiziramo programske jezike s formalnimi matematičnimi metodami.

predavanja, vaje, domače naloge

domače naloge
projekt ali pisni izpit
5 - 10, pri čemer velja, da je pozitivna ocena od 6 - 10

Andrej Bauer:

– LUKŠIČ, Primož, HORVAT, Boris, BAUER, Andrej, PISANSKI, Tomaž. Practical E-Learning for the Faculty of Mathematics and Physics at the University of Ljubljana. Interdisciplinary journal of knowledge & learning objects, ISSN 1552-2210, 2007, vol. 3, str. 73-83 [COBISS-SI-ID 14269529]

– BAUER, Andrej, STONE, Christopher A. RZ: a tool for bringing constructive and computable mathematics closer to programming practice. V: Computation and logic in the real world : Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 18-23, 2007 : proceedings, (Lecture notes in computer science, ISSN 0302-9743, 4497). Berlin, Heidelberg: Springer, cop. 2007, str. 28-42 [COBISS-SI-ID 14631769]

Matija Pretnar:

– PLOTKIN, Gordon, PRETNAR, Matija. Handling algebraic effects. Logical methods in computer science, ISSN 1860-5974, 2013, vol. 9, iss. 4, paper 23 (str. 1-36) [COBISS-SI-ID 16816729]

– PRETNAR, Matija. Inferring algebraic effects. Logical methods in computer science, ISSN 1860-5974, 2014, vol. 10, iss. 3, paper 21 (str. 1-43) [COBISS-SI-ID 17190745]

– BAUER, Andrej, PRETNAR, Matija. An effect system for algebraic effects and handlers. Logical methods in computer science, ISSN 1860-5974, 2014, vol. 10, iss. 4, paper 9 (str. 1-29). http://arxiv.org/pdf/1306.6316 [COBISS-SI-ID 17191001]

Alexander Keith Simpson:

– AWODEY, Steve, BUTZ, Carsten, SIMPSON, Alex, STREICHER, Thomas. Relating first-order set theories and elementary toposes. Bulletin of symbolic logic, ISSN 1079-8986, 2007, vol. 13, no. 3, str. 340-358 [COBISS-SI-ID 17096537]

– SIMPSON, Alex. Computational adequacy for recursive types in models of intuitionistic set theory. Annals of pure and applied Logic, ISSN 0168-0072. [Print ed.], 2004, vol. 130, iss. 1-3, str. 207-275 [COBISS-SI-ID 17117017]

– SIMPSON, Alex. A characterization of the least-fixed-point operator by dinaturality. Theoretical computer science, ISSN 0304-3975, 1993, vol. 118, iss. 2, str. 301-314 [COBISS-SI-ID 17181017]