No description available.

The readability of source code is essential for software maintenance. Since maintenance is an ongoing process, which is estimated to be 70 percent of the software development life cycle's total costs, it cannot be deprioritized. The readability of source code is likely to affect the program comprehension, which may help or create problems in the maintenance of the software. How different code features and functions affect the readability of source code have previously been investigated, and readability metrics have been developed. The project was initiated because of the lack of research on how programming knowledge and statically compared to dynamically typed programming languages affect the readability of the source code. A survey was conducted and included 21 computer science students with various programming knowledge, each rating eight code snippets, making it in total 168 ratings. The results showed that the type of programming language could improve the readability of source code. The results also showed that programming knowledge does not have a correlation with the ability to read source code.

In this thesis, we study the broadcast scheduling algorithms in a dynamic environment with set-typed data requests. We sketch the dimensions of broadcasting paradigms and build a family of Wp

This study examines gender typing of industrial products in the activity of industrial design. Thus firstly, the meaning of gender, related theories and gender stereotypes have been reviewed through the literature survey in order to pinpoint the stereotypical attributes assigned to men and women through society and culture. Secondly, the effect of the stereotypical gender attributes on the act of possessing products have been examined. In return, a literature survey on the cognitive aspects of design has been conducted in order to question whether these gender attributes might have a similar impact on the design activity. The findings of the literature survey pointed towards categorical information processing theories as an appropriate tool to gender type products and also as a tool to measure the gender qualities of a product. To test the applicability of the methodology of categorization a study has been conducted with industrial designers and industrial design students in which the students were asked to design gender typed products and industrial designers were asked to rate their perceptions of genderedness of the designs. The test revealed the existence of a mental library consisting of categorized images corresponding to stereotypical gender attributes in the individuals, thus preparing the grounds for the use of this process in the industrial design activity.

We study the interplay between dependent types and computational effects, two important areas of modern programming language research. On the one hand, dependent types underlie proof assistants such as Coq and functional programming languages such as Agda, Idris, and F*, providing programmers a means for encoding detailed specifications of program behaviour using types. On the other hand, computational effects, such as exceptions, nondeterminism, state, I/O, probability, etc., are integral to all widely-used programming languages, ranging from imperative languages, such as C, to functional languages, such as ML and Haskell. Separately, dependent types and computational effects both come with rigorous mathematical foundations, dependent types in the effect-free setting and computational effects in the simply typed setting. Their combination, however, has received much less attention and no similarly exhaustive theory has been developed. In this thesis we address this shortcoming by providing a comprehensive treatment of the combination of these two fields, and demonstrating that they admit a mathematically elegant and natural combination. Specifically, we develop a core effectful dependently typed language, eMLTT, based on Martin-L¨of’s intensional type theory and a clear separation between (effect-free) values and (possibly effectful) computations familiar from simply typed languages such as Levy’s Call-By-Push-Value and Egger et al.’s Enriched Effect Calculus. A novel feature of our language is the computational S-type, which we use to give a uniform treatment of type-dependency in sequential composition. In addition, we define and study a class of category-theoretic models, called fibred adjunction models, that are suitable for defining a sound and complete interpretation of eMLTT. Specifically, fibred adjunction models naturally combine standard category-theoretic models of dependent types (split closed comprehension categories) with those of computational effects (adjunctions). We discuss and study various examples of these models, including a domain-theoretic model so as to extend eMLTT with general recursion. We also investigate a dependently typed generalisation of the algebraic treatment of computational effects by showing how to extend eMLTT with fibred algebraic effects and their handlers. In particular, we specify fibred algebraic effects using a dependently typed generalisation of Plotkin and Pretnar’s effect theories, enabling us to capture precise notions of computation such as state with location-dependent store types and dependently typed update monads. For handlers, we observe that their conventional term-level definition leads to unsound program equivalences becoming derivable in languages that include a notion of homomorphism, such as eMLTT. To solve this problem, we propose a novel type-based treatment of handlers via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a family of value terms (the operations). This type internalises Plotkin and Pretnar’s insight that handlers denote algebras for a given equational theory of computational effects. We demonstrate the generality of our type-based treatment of handlers by showing that their conventional term-level presentation can be routinely derived, and this treatment provides a useful mechanism for reasoning about effectful computations. Finally, we show that these extensions of eMLTT can be soundly interpreted in a fibred adjunction model based on the families of sets fibration and models of Lawvere theories.

Det blir allt vanligare med att använda webbläsare som plattform för applikationer istället för de konventionella som måste installeras lokalt. Frågan är hur pass bra JavaScript står sig när det kommer till intensiva och tunga algoritmer såsom sökalgoritmer för spel. Finns det optimeringar som kan förbättra tidsåtgången för sökalgoritmer så att användaren i slutändan inte tröttnar på att det tar för lång tid? Med hjälp av ett antal tekniker såsom Typed Arrays försöker det här arbetet påvisa huruvida Typed Arrays kan användas som optimeringsstrategi för en applikation handskriven i JavaScript för att sänka tidsåtgången. Detta arbete syftar till att utvärdera hur användbart av optimeringsstrategier såsom Typed Arrays påverkar tidsåtgången för en förutbestämd sökväg. Flera versioner av en applikation implementeras för att se vilken optimering som är mest lämpad och utvärderas sedermera genom prestandamätning. Resultatet visar att ingen av de valda optimeringsstrategierna gav någon nämnvärd förbättring utan var till vissa delar en försämring jämfört med referensmätningen.

This thesis presents a critical analysis of normalisation by evaluation as a technique for speeding up compilation of typed functional programming languages. Our investigation focuses on the SML.NET compiler and its typed intermediate language MIL. We implement and measure the performance of normalisation by evaluation for MIL across a range of benchmarks. Taking a different approach, we also implement and measure the performance of a graph-based shrinking reductions algorithm for SML.NET. MIL is based on Moggi’s computational metalanguage. As a stepping stone to normalisation by evaluation, we investigate strong normalisation of the computational metalanguage by introducing an extension of Girard-Tait reducibility. Inspired by previous work on local state and parametric polymorphism, we define reducibility for continuations and more generally reducibility for frame stacks. First we prove strong normalistion for the computational metalanguage. Then we extend that proof to include features of MIL such as sums and exceptions. Taking an incremental approach, we construct a collection of increasingly sophisticated normalisation by evaluation algorithms, culminating in a range of normalisation algorithms for MIL. Congruence rules and alpha-rules are captured by a compositional parameterised semantics. Defunctionalisation is used to eliminate eta-rules. Normalisation by evaluation for the computational metalanguage is introduced using a monadic semantics. Variants in which the monadic effects are made explicit, using either state or control operators, are also considered. Previous implementations of normalisation by evaluation with sums have relied on continuation-passing-syle or control operators. We present a new algorithm which instead uses a single reference cell and a zipper structure. This suggests a possible alternative way of implementing Filinski’s monadic reflection operations. In order to obtain benchmark results without having to take into account all of the features of MIL, we implement two different techniques for eliding language constructs. The first is not semantics-preserving, but is effective for assessing the efficiency of normalisation by evaluation algorithms. The second is semantics-preserving, but less flexible. In common with many intermediate languages, but unlike the computational metalanguage, MIL requires all non-atomic values to be named. We use either control operators or state to ensure each non-atomic value is named. We assess our normalisation by evaluation algorithms by comparing them with a spectrum of progressively more optimised, rewriting-based normalisation algorithms. The SML.NET front-end is used to generate MIL code from ML programs, including the SML.NET compiler itself. Each algorithm is then applied to the generated MIL code. Normalisation by evaluation always performs faster than the most naıve algorithms— often by orders of magnitude. Some of the algorithms are slightly faster than normalisation by evaluation. Closer inspection reveals that these algorithms are in fact defunctionalised versions of normalisation by evaluation algorithms. Our normalisation by evaluation algorithms perform unrestricted inlining of functions. Unrestricted inlining can lead to a super-exponential blow-up in the size of target code with respect to the source. Furthermore, the worst-case complexity of compilation with unrestricted inlining is non-elementary in the size of the source code. SML.NET alleviates both problems by using a restricted form of normalisation based on Appel and Jim’s shrinking reductions. The original algorithm is quadratic in the worst case. Using a graph-based representation for terms we implement a compositional linear algorithm. This speeds up the time taken to perform shrinking reductions by up to a factor of fourteen, which leads to an improvement of up to forty percent in total compile time.

The thesis deals with correctness of a compiler of a simple language featuring exceptions. We present formal semantics, both denotational semantics of a~high-level language and operational semantics of a low-level language for a~simple stack machine. We study the method of stack unwinding and then iteratively, improving upon a naive solution, we present a different method that is structurally recursive and thus suitable for implementation in total dependently typed languages. Finally, we provide an implementation of the compiler in the dependently typed functional programming language Agda, along with a mechanically verifiable proof of adherence of the implementation to the semantics.

As the use of technology for personal, professional, and learning purposes increases, more and more assessments are transitioning from a traditional paper-based testing format to a computer-based one. During this transition, some assessments are being offered in both paper and computer formats in order to accommodate examinees and testing center capabilities. Scores on the paper-based test are often intended to be directly comparable to the computer-based scores, but such claims of comparability are often unsupported by research specific to that assessment. Not only should the scores be examined for differences, but the thought processes used by raters while scoring those assessments should also be studied to better understand why raters might score response modes differently. Previous comparability literature can be informative, but more contemporary, test-specific research is needed in order to completely support the direct comparability of scores. The goal of this thesis was to form a more complete understanding of why analytic scores on a writing assessment might differ, if at all, between handwritten and typed responses. A representative sample of responses to the writing composition portion of a large-scale high school equivalency assessment were used. Six trained raters analytically scored approximately six-hundred examinee responses each. Half of those responses were typed, and the other half were the transcribed handwritten duplicates. Multiple methods were used to examine why differences between response modes might exist. A MANOVA framework was applied to examine score differences between response modes, and the systematic analyses of think-alouds and interviews were used to explore differences in rater cognition. The results of these analyses indicated that response mode was of no practical significance, meaning that domain scores were not notably dependent on whether or not a response was presented as typed or handwritten. Raters, on the other hand, had a more substantial effect on scores. Comments from the think-alouds and interviews suggest that, while the scores were not affected by response mode, raters tended to consider certain aspects of typed responses differently than handwritten responses. For example, raters treated typographical errors differently from other conventional errors when scoring typed responses, but not while scoring the handwritten duplicates. Raters also indicated that they preferred scoring typed responses over handwritten ones, but felt they could overcome their personal preferences to score both response modes similarly. Empirical investigations on the comparability of scores, combined with the analysis of raters’ thought processes, helped to provide a more evidence-based answer to the question of why scores might differ between response modes. Such information could be useful for test developers when making decisions regarding what mode options to offer and how to best train raters to score such assessments. The design of this study itself could be useful for testing organizations and future research endeavors, as it could be used as a guide for exploring score differences and the human-based reasons behind them.

No description available.