1,720,997 research outputs found
[Supporting material] On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control
No full textWe compare the expressive power of three programming abstractions
for user-defined computational effects: Bauer and Pretnar's effect
handlers, Filinski's monadic reflection, and delimited control
without answer-type-modification. This comparison allows a precise
discussion about the relative expressiveness of each programming
abstraction. It also demonstrates the sensitivity of the relative
expressiveness of user-defined effects to seemingly orthogonal
language features.
We present three calculi, one per abstraction, extending Levy's
call-by-push-value. For each calculus, we present syntax,
operational semantics, a natural type-and-effect system, and, for
effect handlers and monadic reflection, a set-theoretic denotational
semantics. We establish their basic metatheoretic properties:
safety, termination, and, where applicable, soundness and
adequacy. Using Felleisen's notion of a macro translation, we show
that these abstractions can macro-express each other, and show which
translations preserve typeability. We use the adequate finitary
set-theoretic denotational semantics for the monadic calculus to
show that effect handlers cannot be macro-expressed while preserving
typeability either by monadic reflection or by delimited control.
Our argument fails with simple changes to the type system such as
polymorphism and inductive types. We supplement our development with
a mechanised Abella formalisation
Accompanying material for the article 'no value restriction is needed for algebraic effects and handlers'
No full textWe present a straightforward, sound, Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. The soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and many programming examples can be recast to use effect handlers instead of these effects. This file formalises in Twelf the calculus and its soundness proof
An Introduction to Algebraic Effects and Handlers. Invited tutorial paper
No full textAbstractThis paper is a tutorial on algebraic effects and handlers. In it, we explain what algebraic effects are, give ample examples to explain how handlers work, define an operational semantics and a type & effect system, show how one can reason about effects, and give pointers for further reading
Calculation of Solvency Capital Requirement for Insurance and Reinsurance Undertakings According to the Standard Formula in programming language R
Full text linkKernel methods
No full textV diplomskem delu predstavimo jedrne funkcije in njihovo uporabo v jedrnih metodah. Predstavimo splošen problem binarne klasifikacije in njegovo rešitev v primeru homogene linearne ločljivosti podatkov. Preko Coverjevega izreka spoznamo potrebo po jedrnih funkcijah. Ogledamo si Hilbertove prostore z reproducirajočim jedrom ter dokažemo Moore–Aronszajnov in reprezentacijski izrek. Navedemo nekaj primerov jedrnih funkcij in pravila za sestavljanje novih. Podrobneje spoznamo tri pomembne jedrne metode: metodo podpornih vektorjev, analizo glavnih komponent in Gaussove procese. Spoznamo tudi povezavo med Gaussovimi procesi in drugimi metodami strojnega učenja.In this work we present kernel functions and their use in kernel methods. We state the general problem of binary classification and its solution in case of homogeneously linearly separable dataset. Through Cover\u27s theorem we recognize the need for kernel functions. We present reproducing kernel Hilbert spaces and prove the Moore–Aronszajn and representer theorems. We take a look at a few examples of kernel functions and the rules for constructing new ones. We cover three important kernel methods in depth: support vector machines, principal component analysis and Gaussian processes. We also present the link between Gaussian processes and other machine learning methods
Analysis and Visualization of Real Estate Date in Slovenia
Full text linkV magistrskem delu bomo najprej predstavili nepremičninske evidence v Sloveniji. Na kratko bomo predstavili razloge za vzpostavitev, njihov zgodovinski razvoj in povezanost med njimi. Na koncu bomo pojasnili, kje pri trenutni ureditvi lahko pride do napačnih podatkov.
V nadaljevanju bomo predstavili osnovne pojme in se osredotočili na najmlajšo nepremičninsko evidenco, register nepremičnin. Opisali bomo njegov podatkovni model in opravili osnovno analizo atributnih podatkov ter jih na podlagi ugotovitev poskusili vizualizirati. Menimo, da so nekateri podatki v evidencah napačni, zato jih bomo skušali odkriti in predlagali možnosti za njihovo odpravo. Menimo, da do napak prihaja pri vnosu in zaradi povezovanja z drugimi evidencami. Predlagali bomo pravila, kako se napakam izogniti ter podali možnosti uporabe sodobnih tehnologij, ki bi nam pri tem lahko pomagale.This thesis deal with real estate records in Slovenia. Firstly, it briefly presents reasons for their establishment, their historical development and their interconnectedness. Secondly, the thesis discusses how current real estate record regulations might bring about faulty data.
In the main part of the thesis, main technical terms are explained, with the focus on those related to the most recent version of real estate records - the real estate registry. Its data model is described and an analysis of attributive data is carried out. Based on the findings, a visualisation of data is presented. We believe that some data in the records is faulty, so we try and discover the errors and search for solutions on how to eliminate them. We believe that the errors occur due to incorrect data input and due to interconnectedness between different records. We suggest some techniques for eliminating the inaccuracies, most of which are carried out with the help of modern technologies
Uporaba teorij algebrajskih učinkov
Full text linkAlgebraic effects are an established method of implementing effectful behaviour in functional programming languages. Computational effects are represented by operations and implemented through effect handlers. An effect theory consists of a type signature and a set of equations describing the behaviour of effect invocations. All effect handlers are required to adhere to the prescribed effect theory, meaning that they do not differentiate between two programs considered equal in the given theory. The standard approach to algebraic effects assumes a global effect theory, so all handlers need to respect the same set of equations. This often becomes very restricting in terms of suitable handlers and therefore most contemporary work focuses on theories that contain no equations. Discarding equations allows for a wider variety of viable handlers but drastically reduces the capabilities to reason about properties of effectful code.
In the thesis we present the language EEFF that relaxes the single theory limitation by using local effect theories, allowing the use of different theories in different parts of the program, even when pertaining to effects with the same signature. This alleviates the issues of global effect theories while providing all benefits of equations. The type system is upgraded to track theory information, allowing for safe use of handlers and ensuring their correctness at the relevant theory. Proofs of handler correctness are done in a logic that is coupled with the type system. The type system can be coupled with different logics, granting the option to select a logic suitable for the problems at hand. The soundness of a logic is established with respect to a denotational semantics based on partial equivalence relations.
The safety theorems of EEFF are formalised in the proof assistant Coq, and the implementation of EEFF is an extension of the language Eff. The formalisation also doubles as a reasoning tool for programs with algebraic effect theories and features two different logics to choose from, both of which are shown to be sound. Multiple examples throughout the thesis showcase the benefits of local algebraic theories.Algebrajski učinki so uveljavljena metoda za modeliranje računskih učinkov v funkcijskem programiranju. Učinke predstavimo z operacijami, pomen pa jim dodelimo s prestrezniki. Teorije algebrajskih učinkov so sestavljene iz signature, ki poda tipe operacij, in enačb, ki opisujejo njihovo obnašanje. Vsi prestrezniki morajo biti skladni s predpisano teorijoprestreznik ne sme razlikovati med programi, ki jih v dani teoriji smatramo za enake. Teorije učinkov so običajno globalne, torej morajo vsi prestrezniki spoštovati isto množico enačb, kar omeji nabor možnih prestreznikov. Mnogo kasnejših pristopov zato enačbe odmisli, kar sicer olajša uporabo prestreznikov, vendar močno omeji možnosti dokazovanja lastnosti programov ob prisotnosti računskih učinkov, kjer enačbe igrajo ključno vlogo.
V doktorskem delu predstavimo jezik EEFF, ki z uporabo lokalnih teorij učinkov omili omejitve enotne teorije učinkov, saj omogoči uporabo različnih teorij v različnih delih programa. Za varnost poskrbi sistem tipov, nadgrajen z zmožnostjo sledenja teorijam učinkov, ki omogoča varno uporabo prestreznikov. Sistemu tipov je pridružena logika, v kateri preverjamo pravilnost prestreznikov. Za logiko imamo na voljo več možnosti, kar nam omogoča izbiro najprimernejše logike glede na problem. Zdravost logike določimo z uporabo denotacijske semantike, ki temelji na delnih ekvivalenčnih relacijah.
Jezik EEFF je formaliziran v dokazovalnem pomočniku Coq in implementiran kot razširitev programskega jezika Eff. Formalizacija hkrati služi kot orodje za dokazovanje ekvivalence programov in vsebuje dve različni logiki, za kateri pokažemo zdravost. V doktorskem delu podamo več primerov, ki predstavijo prednosti uporabe lokalnih teorij algebrajskih učinkov
Using Rust types for safely controlling devices
No full textV magistrskem delu je predstavljen razvoj nove metode za programiranje sistemov, zasnovanih na končnih avtomatih. Metoda se lahko uporabi pri programiranju vgrajenih sistemov, ki jih lahko predstavimo s končnimi avtomati, kot so pametne luči, robotske kosilnice in polnilnice za električna vozila. Razvita metoda omogoča pisanje končnega avtomata kot zaporedje akcij na srečni poti - to je privzet scenarij, kjer se ne zgodi nobena napaka - in izboljša varnost programske kode. To doseže s pomočjo programskega jezika Rust, njegovih tipov, asinhronega programiranja ter sistema lastništva. V delu je predstavljena tudi implementacija razvite metode v obliki odprtokodne knjižnice.The master\u27s thesis presents the development of a new method for programming finite-state machine based systems. The method can be used for programming embedded systems that can be represented by finite-state machines, such as smart lights, robotic lawn mowers and electric vehicle charging stations. The developed method allows writing a finite-state machine as a sequence of actions on happy path scenario - that is, the default scenario where no errors occur - and improves the security of the code. This is achieved with the help of the Rust programming language, its types, asynchronous programming and the ownership system. The work also presents the implementation of the developed method in the form of an open-source library
Parallelisation of graph algorithms in functional programming languages
No full textDiplomska naloga obravnava paralelizacijo grafovskih algoritmov v funkcijskih programskih jezikih, s poudarkom na OCamlu in uporabi knjižnice Domainslib. Delo se osredotoča na razvoj in analizo paralelnih različic klasičnih algoritmov, kot so iskanje v širino (BFS), Dijkstrov algoritem in Floyd-Warshallov algoritem. Glavni cilj je primerjava učinkovitosti paralelnih in sekvenčnih implementacij teh algoritmov v kontekstu funkcijskega programiranja. Analiza je pokazala, da paralelna implementacija lahko izboljša učinkovitost, še posebej pri obsežnih grafih. Kljub temu pa smo identificirali tudi omejitve pri izboljšavah učinkovitosti zaradi same narave paralelnega izvajanja.This thesis addresses the parallelisation of graph algorithms in functional programming languages, with a focus on OCaml and the use of the Domainslib library. The work concentrates on developing and analyzing parallel versions of classical algorithms, such as breadth-first search (BFS), Dijkstra\u27s algorithm, and the Floyd-Warshall algorithm. The primary goal is to compare the effectiveness of parallel and sequential implementations of these algorithms in the context of functional programming. The analysis showed that parallel implementation can improve efficiency, especially in extensive graphs. However, improvements in efficiency are also identified to have limitations due to the inherent nature of parallel execution
- …
