20.500.12556/RUL-150138 Operacijska semantika za jezik s časovno omejenimi viri magistrsko delo Operational semantics for temporal resources Lambda račun je eden izmed osnovnih matematičnih modelov računanja, kjer uporabljamo le spremenljivke, funkcije (abstrakcije) in aplikacije funkcij. Lahko ga razširimo s tipi in tako dobimo tipizirani lambda račun, ki je jedro funkcijskih programskih jezikov. Tipi v jeziku zagotavljajo varnost, saj preprečujejo, da bi programer na primer seštel število in niz. V delu predstavimo problem, ki nastane pri uporabi jezika v industriji, kjer mora med določenimi procesi preteči dovolj časa. Želimo si, da to reši že sistem tipov. Obstoječi sistemi, kot je OCamlov, tega ne omogočajo. Sistem tipov razširimo z modalnim tipom, ki zagotovi, da vira ne uporabimo, če ni prej preteklo dovolj časa. Za pravilno delo s tovrstnim tipom poskrbita operaciji odvijanje in zavijanje. V tem delu za tovrstni jezik podamo operacijsko semantiko, kjer si za pravilno delo s časovno omejenimi viri pomagamo s stanjem. Dokažemo izrek o varnosti, torej da bo vsak program napisan v tem jeziku ohranil tip in da bo v vsakem trenutku naredil korak, ali pa se ustavil. V delu definiramo enačbe za teorijo enačb za delo s časovno omejenimi viri in dokažemo, da je operacijska semantika skladna s teorijo enačb. Vsi rezultati, razen nekaterih primerov v dokazu skladnosti, so formalizirani z dokazovalnim pomočnikom Agda. Lambda calculus is one of the fundamental mathematical models of computation, where we utilize variables, function abstractions, and function applications. Further, it can be extended with types, giving rise to the typed lambda calculus, which forms the core of functional programming languages. Types in a language provide safety by preventing, for example, the addition of a number and a string. In this work, we present one of the problems that arises when using a functional language in production, where certain processes need to wait for a specified amount of time to pass. We would like the type system to address this problem. A simple type system, as found in OCaml, does not facilitate this requirement, so the type system can be extended with a modal type, which ensures that a resource is not used unless enough time has passed. For proper handling of this type, unboxing and boxing operations are introduced. In this work, we provide stateful operational semantics for this kind of language, where we use state to handle temporal resources correctly. We prove a safety theorem, ensuring that every program written in this language preserves its type and either steps or halt at every moment. We also define an equational theory for this stateful view of resource useage and prove that evaluation in operational semantics respects the equational theory. All results, apart from some cases of the soundness theorem, have also been formalized using the proof assistant Agda. lambda račun časovno omejeni viri modalni tipi izrek o varnosti teorija enačb skladnost formalizacija lambda calculus temporal resources modal type safety theorem equational theory soundness formalization true false false Slovenski jezik Angleški jezik Magistrsko delo/naloga 2023-09-14 08:15:19 2023-09-14 08:15:21 2024-05-29 10:39:28 0000-00-00 00:00:00 2023 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 135960 164319747 9573.pdf 9573.pdf 1 375CB33D47C76E6969F6949B7D02F3DE 206433514142012db37fe26bfab928a81f07ef1d6e917be5bda5ff3b0214db62 15b9badb-52c6-11ee-b233-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=174686 9574.zip 9574.zip 1 9F93646A6E7E9E19E4011FA6838C0D45 3ae4cc48cdbcf6a8d456a54be8d6f52fc77ce3abf53dc873d2077c9a0f67231c 15ba0f34-52c6-11ee-b233-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=174687 Fakulteta za matematiko in fiziko 0 0 0