Data- och informationsteknik (CSE) // Computer Science and Engineering (CSE)
Använd denna länk för att länka till samlingen:
Vi utbildar för framtiden och skapar samhällsnytta genom vår forskning som levandegörs i nära samarbete med näringslivet. Vi bedriver forskning inom computer science, datateknik, software engineering och interaktionsdesign - från grundforskning till direkta tillämpningar. Institutionen har en stark internationell prägel och är delad mellan Chalmers och Göteborgs universitet.
För forskning och forskningspublikationer, se https://research.chalmers.se/organisation/data-och-informationsteknik/
We are engaged in research and education across the full spectrum of computer science, computer engineering, software engineering, and interaction design, from foundations to applications. We educate for the future, conduct research with high international visibility, and create societal benefits through close cooperation with businesses and industry. The department is joint between Chalmers and the University of Gothenburg.
Studying at the Department of Computer Science and Engineering at Chalmers
For research and research output, please visit https://research.chalmers.se/en/organization/computer-science-and-engineering/
Browse
Browsar Data- och informationsteknik (CSE) // Computer Science and Engineering (CSE) efter Författare "Abel, Andreas"
Visar 1 - 16 av 16
Sökresultat per sida
Sortera efter
- PostA Formal Semantics for Javalette in the K framework(2022) Burak Bilge, Yalcinkaya; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Abel, Andreas; Myreen, MagnusThis thesis is about developing an executable formal semantics for Javalette in the K framework. Javalette is an imperative programming language. Its syntax is formally specified using BNF (Backus-Naur form) notation, but it does not have a formal semantics. The semantics of the language is informally documented in English. Javalette has several extensions that enrich the language’s syntax and semantics with new types, statements, and expressions. K is a toolset for programming language design and implementation. It provides a specification language for formally defining syntax and semantics. From these definitions, K automatically generates various tools such as parsers, interpreters, model checkers, and deductive verifiers. The purpose of this project is to develop a complete formal semantics for the Javalette language, design an architecture for extending the language modularly and implement language extensions, find and resolve undefined behaviors in the language, and use the formal semantics to develop an input fuzzer for testing Javalette programs and implementations.
- PostA Parametric Fitch-Style Modal Lambda Calculus(2023) Forsman, Axel; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Abel, Andreas; Valliappan, NachiappanThe necessity modality, denoted by , where the focus lies, has been applied to model staged computations, compartmental purity in functional languages, and more. So called Fitch-style modal deduction, where modalities are eliminated by opening a subproof, and introduced by shutting one, has been adapted for lambda calculi. Different modal logics may be encoded via different open and shut rules. Prior work [1] has given normalization proofs for four Fitch-style formulations of lambda calculi with different modalities, which required repeating the proofs for each individual calculus. A parametric Fitch-style modal lambda calculus generalizing the variants is presented, in order to avoid the repetition and ease further extensions.
- PostA Reflexive Graph Model of Sized Types(2020) Limperg, Jannis; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Hughes, John; Abel, AndreasSized types are a type-based termination checking mechanism for dependently typed languages. Compared to syntactic termination checkers, sized types make termination checking more modular and allow for an elegant treatment of coinductive and nested data types. This thesis investigates λST, a simply-typed lambda calculus with sized types similar to those of Agda. Its primary contribution is a relationally parametric denotational semantics for λST in the form of a reflexive graph model. In this model, sizes are irrelevant: they do not affect the result of any computations. The calculus and model are fully formalised in Agda (without sized types).
- PostA Syntax for Composable Data Types in Haskell, A User-friendly Syntax for Solving the Expression Problem(2023) Romeborn, Anna; Albers, Fredrik; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Abel, Andreas; Broberg, NiklasThe expression problem is the problem of designing a programming language such that it has both extensible data types and extensible sets of functions over those data types. This means that it should be possible to add new functions, new variants to a data type, and function cases for these new variants, without modification or recompilation of existing code. There exist a number of different approaches to solving the expression problem, which have different qualities in expressiveness or simplicity. In this thesis, we have designed a syntax, with an accompanying transformation into compilable code, that acts as a solution to the expression problem in Haskell. By designing this syntax, we can make simplifications that would not be possible for solutions written directly in Haskell. In particular, we can, behind our syntax, abstract away some syntactic overhead that can be generated by the transformation. To demonstrate that our designed syntax is feasible and works as an extension to Haskell, we have implemented the transformation, which transforms code written using our syntax into code that uses the Haskell library compdata. That library is an existing solution to the expression problem, and is based on another solution:Data Types à la Carte. Both of these solutions share many similarities in semantics with our syntax. Similarly to compdata and Data Types à la Carte, data types in our syntax are composable; that is, variants of a data type are manually combined to form a type with a fixed set of possible variants. We introduce a new concept, called categories, with the purpose of grouping variants and compositions of data types and simplifying the syntax into one closer to that of regular data types. This means that compositions of variants can only be formed of variants belonging to the same category, as opposed to freely being able to combine any variants. Again, similar to compdata and Data Types à la Carte, functions over composable data types are extended automatically in our syntax. This means that a function can be used for a variant of the data type as long as the function has a case defined for the variant. Through the introduction of categories and the abstractions possible through the transformation, we are able to conclude that our syntax provides several improvements compared to existing solutions to the expression problem in Haskell.
- PostAn Agda Formalisation of Modalities and Erasure in a Dependently Typed Language(2021) Eriksson, Oskar; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Jansson, Patrik; Abel, AndreasModal types extend the expressivity of types by giving them different interpretations depending on the used modality. In this thesis, we develop a general modality structure in the setting of a dependently typed language, notably containing dependent products and sums as well as natural numbers, based on the work of Abel and Bernardy [1]. The modality structure is based on a semiring, the elements of which are used as annotations on terms and whose algebraic properties form the basis for the modal type system. In addition, we instantiate the general modality structure to a modality for erasure in which annotations are interpreted as either computationally relevant, indicating that the annotated term is used during evaluation, or computationally irrelevant, indicating that the marked term is not useful during evaluation. Based on this interpretation, we define an extraction function that translates terms to an untyped lambda calculus, removing terms that have been marked for erasure. Using a logical relation between terms of the two languages we then prove the extraction function to be sound with respect to the semantics of the languages in the special case of natural numbers.
- PostAn Agda scope checker implemented in Agda(2023) Gazzetta, Francesco; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Jansson, Patrik; Abel, AndreasAgda [1] is a Haskell-style, purely functional, dependently typed programming language and theorem prover. Scope checking is the process of analyzing the Abstract Syntax Tree (AST) of a program and resolving all references to symbols by connecting them to the corresponding declarations of said symbols. The Agda scope checker – as well as the rest of the compiler – is written in Haskell, and does not include any proof about the reachability of declarations. In this thesis, we present a scope checker for the Agda language, written in Agda itself, and prove the correctness of its name resolution algorithm with reference to the reachability properties of the Agda language. The result of this scope checking pass is a correct by construction AST that contains a proof that the syntax is well-scoped represented as paths from references of names (eg. x) to declarations (eg. x = ...).
- PostComparison of Machine Learning Approaches Applied to Predicting Football Players Performance(2020) Lindberg, Adrian; Söderberg, David; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Abel, Andreas; Seger, Carl-Johan; Yu, YinanThis thesis investigates three machine learning approaches: Support Vector Machine (SVM), Multi-Layer Perceptron (MLP) and Long Short-Term Memory (LSTM) on predicting the performance of an upcoming match for a football player in the English Premier League. Each approach is applied to two problems: regression and classification. The last four seasons of English Premier League is collected and analyzed. Each approach and problem is tested several times with different hyperparameters in order to find the best performance. We evaluate on five game weeks by picking a lineup for each model that is then measured by its collective score. The results indicate that regression outperforms classification, with LSTM being the best performing model. The score ends up outperforming the average of all managers during the evaluated period in the online football game, Fantasy Premier League. The findings could be used to assist in providing insight from historical data that might be too complex to find for humans.
- PostConstructing a Game Modelled After Logic and Proofs(2019) Burström, Elias; Källman, Jonatan; Ngo, Tuyen; Nordén, Felix; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Ahrendt, Wolfgang; Fjeld, Morten; Knutsson, Sven; Abel, AndreasLogiskt resonemang spelar en viktig roll för mänskligt beteende och används i många aspekter av vardagslivet. Det är en del av ämnen såsom naturliga språk, matematik och programmering. Allmänhetens knappa kunskap om ämnet speglar däremot inte dess betydelse. I enklare situationer behöver denna brist på kunskap inte vara ett problem, men i mer komplexa situationer kan en avsaknad av kunskap leda till felaktiga resonemang. En förklaring till denna kunskapsbrist kan vara avsaknaden av logik i den allmänna skolan, då ämnet huvudsakligen lärs ut på universitetsnivå. Detta problem skulle kunna mildras med hjälp av Tenjin, ett smartphone-spel baserat på klassisk satslogik i formen av sekventiell analys. Tenjin ämnar göra inlärningsprocessen av formell logik tillgänglig för individer i åldrarna 13–25 genom att ersätta den formella syntaktiska notationen med ett intuitivt, rymd-inspirerat användargränssnitt. För att agera på ett konceptuellt plan för Tenjin, så beskriver denna tes en utvecklings- och designprocess som resulterar i en precis mjukvarurepresentation för en delmängd av klassisk satslogik, samt en testad och intuitiv visualisering för användaren att interagera med. Design av den visuella representationen genomfördes med hjälp utav inkrementell testning. Först testades varje kandidat genom prestanda-tester som baserades på bevis av olika svårighetsgrad. Om en kandidat klarade prestanda-testerna, så testades den sedan genom pappers-prototyptester med riktiga användare. Utveckling av mjukvaran utfördes med hjälp av välgrundade utvecklingsprinciper och verktyg, såsom S.O.L.I.D-principerna och diverse designmönster. Efter en genomgående modelleringsprocess av problemdomänen användes programmeringsspråket C# samt ramverken .NET och Unity för att skriva kodbasen.
- PostDecision provenance in a real-time system with microservice architecture(2022) Willim, Daniel; Ljungdahl, Erik; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Abel, Andreas; Russo, AlejandroThis thesis investigates the feasibility of decision provenance, by implementing it in Carmenta TrafficWatch, a real-time system with a microservice architecture. We add provenance by creating a separate service that listens to the message-bus and stores all events and potential changes to those events. This provenance information can later be queried by other services. To have provenance of how events interact with each other, we also implement a system for event aggregation. Our findings indicate that adding provenance to real-time systems with microservice architecture will not impact the overall performance of the system significantly, and is a viable solution to add accountability and increase the understanding of complex systems.
- PostLayout Syntax Support in the BNF Converter(2023) Burreau, Beata; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Ranta, Aarne; Abel, AndreasMany programming languages, such as Haskell and Python, use layout as part of their syntax. We can expect future programming languages to also be layoutsensitive. Therefore, the toolchains for implementing programming languages must support layout-sensitive languages. This thesis presents a declarative approach to describing layout-sensitive languages and parsing programs written in them. We reserve the terminals newline, indent, and dedent for describing layout syntax in BNF grammar and provide an algorithm for representing the layout of a program with these terminals, before parsing it. By verbalising layout syntax this way, mainstream parser generators, and their parsing algorithms, can be used. This approach is successfully implemented in BNF Converter (BNFC), a tool that generates a compiler front-end from a context-free grammar in Labelled BNF (LBNF) form. With a special kind of LBNF rule, called pragma, it is possible to declare global layout syntax rules, such as the offside rule, which affects the insertion of layout terminals by the aforementioned algorithm. The reserved terminals and the pragmas can together describe popular layout syntax. Furthermore, both purely layout-sensitive languages and those mixing layoutsensitive and insensitive syntax are describable in LBNF.
- PostNanoPython - Researching the Feasibility of Running Python Scripts on Arduino Using a Virtual Machine(2020) CAMPBELL, TOBIAS; STRÅLMAN, KARL; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Lundin, Peter; Abel, Andreas; Bergholm, BjörnVirtualization today is a prominent method of both deploying and maintaining applications at a low cost. Various types of virtual machines exist and are used in different fields of computer science. Searching for new innovative ways to deploy tests, Swedish consultancy firm Broccoli wants to research the feasibility of running Python on an embedded system. This thesis primarily focuses on language virtual machines, the compilation involved and researching the feasibility of developing a Python virtual machine for a particular embedded system development board, an Arduino Uno. Starting with a subset of the Python grammar, a bytecode compiler written in Java was developed with the ANTLR tool. Meanwhile, a virtual machine running the compiler-generated bytecode was developed using C++. By adding small fragments to the grammar and accordingly writing additional code to account for this, more functionality was added to both the compiler and the virtual machine. By utilizing tests, functionality of the project could be preserved. The compiler runs the whole process of language processing, including lexing, parsing and code generation. It then generates code in a specific binary file format. A binary file can then be interpreted by the virtual machine. This enables the execution of simple Python scripts on both PC and the chosen system, without regard to optimization for neither compilation nor execution. Although not perfect, the current implementation does run on both systems. Some problems include the limited memory space of the Arduino and the lack of support for important language-defining constructs. Despite the drawbacks, with further improvements the current implementation may be used in the future as a means to rapidly deploy tests, which is of interest to Broccoli.
- PostNormalization for Type Theory with an Impredicative Universe(2024) Xie, Zongpu; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Abel, Andreas; Coquand, ThierryThis thesis presents a novel proof of canonicity and normalization for a type theory a proof relevant impredicative universe and a hierarchy of predicative universes. The proof uses Artin gluing, and is structured in a modular way that makes it easier to extend to new type formers.
- PostOn Definability and Normalization by Evaluation in the Logical Framework(2019) Ramcke, Frederik; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Danielsson, Nils Anders; Abel, AndreasThe question of definability asks to characterise what objects of the meta-theory are definable by a given calculus; for example, the untyped -calculus characterises exactly the Turing-computable functions. This thesis gives a characterisation of LF-definability—definability in a variant of the Edinburgh Logical Framework—in terms of a notion of Kripke predicates. The constructions in this thesis are heavily inspired by, and generalise, those by Jung and Tiuryn, who gave a definability result for the simply-typed -calculus in ‘A New Characterization of Lambda Definability’.
- PostPolynomial Functors in Agda: Theory and Practice(2023) Jörgensson, Marcus; Muricy Santos, André; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Abel, Andreas; Cherubini, FelixThe category of polynomial functors - Poly - has been studied for over two decades and is well known for its relevance to computer science [1] and deep mathematical structure [2]. In recent years, new interpretations of Poly have been found in dynamical systems theory [3]. This thesis formalizes Poly in Cubical Agda and showcases its use in dynamical systems, contributing to the Poly code ecosystem. The first part, theory, formalizes the category Poly itself and many of its categorical constructs, including the initial and terminal objects, product, coproduct, equalizer, composition and parallel product. Then Chart is formalized, together with its own categorical constructs. Finally, Poly and Chart morphisms are combined via commuting squares. The second part, practice, builds upon the theory by using these categories to implement dynamical systems. It covers how morphisms in Poly represent dynamical systems, how polynomials act as interfaces, how systems are wired together, how behavior is installed into wiring diagrams, and how to run systems arriving at concrete programs. Many dynamical system examples are given, such as a Fibonacci sequence generator, the Lorenz system, the Hodkgin-Huxley model, and an Echo-State Network that learns the Lorenz dynamics. Commuting squares are used as a way of showing that one dynamical system can be made to simulate another.
- PostSecuring Electronic Exam Environments(2023) Cronqvist, Daniel; Kortesaari, Saga; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Abel, Andreas; Ahmadpanah, Mohammad M.Electronic exams have gained widespread popularity due to their convenience and advantages, particularly in courses involving writing or programming assessments. However, along with their benefits, electronic exams also pose the risk of facilitating cheating, especially when examinees are allowed to use their own devices. To ensure that in-hall bring-your-own-device (BYOD) electronic exams are as secure as their traditional paper-based counterparts, significant measures must be taken to secure the exam environment. This study focuses on two types of e-exam environments: software-based and OS-based. The thesis presents a comprehensive threat modeling process using the Quantitative Threat Modeling Method (QTMM) to identify various cheating-related threats. Based on these findings, the research proposes eight new design principles to guide developers in creating robust and secure e-exam environments as part of their design strategy. These principles are then evaluated through a case study conducted on a popular e-exam environment, Safe Exam Browser (SEB). The case study reveals several vulnerabilities and successful attacks, highlighting that six out of the eight proposed design principles were not adhered to. To address this problem, the thesis presents a novel design proposal for Safe Exam Browser that aligns with the suggested design principles. Implementation of this proposal would effectively address many of the preventable threats, including a significant design flaw. Lastly, the thesis explores how well both software-based and OS-based e-exam environments can mitigate threats by following these design principles. By emphasizing the importance of robust security measures in e-exam environments and providing practical recommendations, this research contributes to the ongoing efforts to enhance the integrity of electronic examinations.
- PostTowards Normalization by Evaluation for Erlang(2023) Agrell, Carl; Yang, Haohan; Chalmers tekniska högskola / Institutionen för data och informationsteknik; Chalmers University of Technology / Department of Computer Science and Engineering; Abel, Andreas; Valliappan, NachiappanNormalization by Evaluation (NbE) is a technique to extract the normal form of a 𝜆-calculus term. Originally targeting pure 𝜆-calculus, the algorithm can be extended and adjusted to work on more practical call-by-value programming languages. We implement NbE for a fragment of Erlang, starting at the Moggi’s semantics framework of computational lambda calculus, and largely inspired by Filinski’s research. The result shows that our normalizer can be applied on programs with rich semantics, and can potentially be extended to perform partial evaluation.