Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Type System for Data Flow and Alias Analysis in ReScript

Nicky Ask Lund, Hans Hüttel

TL;DR

This paper presents a sound type system for data-flow analysis for a subset of the ReScript language, more specifically for a lambda-calculus with mutability and pattern matching.

Abstract

ReScript is a strongly typed language that targets JavaScript, as an alternative to gradually typed languages, such as TypeScript. In this paper, we present a sound type system for data-flow analysis for a subset of the ReScript language, more specifically for a lambda-calculus with mutability and pattern matching. The type system is a local analysis that collects information about variables that are used at each program point as well as alias information.

A Type System for Data Flow and Alias Analysis in ReScript

TL;DR

This paper presents a sound type system for data-flow analysis for a subset of the ReScript language, more specifically for a lambda-calculus with mutability and pattern matching.

Abstract

ReScript is a strongly typed language that targets JavaScript, as an alternative to gradually typed languages, such as TypeScript. In this paper, we present a sound type system for data-flow analysis for a subset of the ReScript language, more specifically for a lambda-calculus with mutability and pattern matching. The type system is a local analysis that collects information about variables that are used at each program point as well as alias information.

Paper Structure

This paper contains 17 sections, 3 theorems, 26 equations, 3 tables.

Table of Contents

  1. Introduction
  2. A fragment of ReScript
  3. Syntax
  4. The binding model
  5. Keeping track of dependencies
  6. Collecting semantics
  7. A type system for data-flow analysis
  8. An overview of the type system
  9. Types
  10. The binding model of the type system
  11. The type system
  12. Soundness
  13. Type rules for values
  14. Notions of agreement
  15. The soundness theorem
  16. ...and 2 more sections

Key Result

Lemma 1

Suppose $e^p$ is an occurrence, that and $x^{p_1}\in \textrm{dom}(w')\backslash \textrm{dom}(w)$. Then $x\notin fv(e^{p})$

Theorems & Definitions (26)

  • Example 1
  • Definition 1: Dependency function
  • Example 2
  • Definition 2: Occurring program points
  • Definition 3
  • Example 3
  • Definition 4: Immediate predecessor
  • Definition 5
  • Example 4
  • Definition 6: Type base for aliasing
  • ...and 16 more