Data-flow analysis of dependencies and aliases for a functional programming languages
Translated title
Data-flow analyse for afhængigheder og aliasering for et funktionelt programmeringssprog
Author
Lund, Nicky Ask
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-16
Pages
56
Abstract
ReScript is a strongly typed programming language that compiles to JavaScript, offered as an alternative to gradually typed languages such as TypeScript. Although it is built on OCaml, ReScript has its own build system and deep JavaScript integration, so there is little formal analysis of the language. Its tooling includes an experimental analyzer that can detect dead code and assess termination (whether programs stop). Data-flow analysis—used for decades in compiler optimization—tracks how values move through a program. In languages with mutable memory locations, such analysis must account for aliasing, when different names refer to the same location. This thesis presents a type system for data-flow analysis for a subset of ReScript, modeled as a lambda calculus with mutability and pattern matching. We define the language’s syntax and semantics and extend the semantics with a data-flow interpretation. Our type system performs a local analysis that records which variables are used and captures alias information. We relate the binding models of the semantics and the type system, and we show that the type system provides a sound approximation of dependencies and aliasing.
ReScript er et stærkt typet programmeringssprog, der oversætter til JavaScript og fungerer som et alternativ til gradvist typede sprog som TypeScript. Selvom ReScript bygger på OCaml, har det sit eget byggesystem og en tæt integration med JavaScript, og der findes derfor kun begrænset formel analyse af sproget. Værktøjskæden omfatter dog et eksperimentelt analyseværktøj, der kan finde dødkode og vurdere, om programmer terminerer (stopper). Dataflowanalyse – som i årtier har været brugt i compilere – sporer, hvordan værdier bevæger sig gennem et program. I sprog med mutable (ændrbare) hukommelsesplaceringer skal analysen tage højde for aliasing, det vil sige når flere navne refererer til den samme placering. I denne afhandling præsenterer vi et typesystem til dataflowanalyse for en delmængde af ReScript, modelleret som en lambda-kalkule med mutabilitet og mønster‑matchning. Vi opstiller sprogets syntaks og semantik og udvider semantikken med en semantisk dataflowanalyse. Vores typesystem udfører en lokal analyse, der samler information om, hvilke variabler der bruges, samt alias-information. Vi relaterer bindingsmodellerne for semantikken og typesystemet og viser, at typesystemet giver en sikker tilnærmelse af afhængigheder og alias-information.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords