Bounded-construction-types for functional reactive programming / Akihiko Yokoyama, Sosuke Moriguchi, Takuo Watanabe.

We introduce a new type system to Emfrp, a functional reactive programming language designed for resource-constrained embedded systems. To ensure such property that the language can statically determine the amount of runtime memory and guarantee the termination of reactive actions, it disallows the use of recursive data types and functions. However, such restrictions often impose unnatural representations of data structures and algorithms used in various applications. Our new type system, named Bounded-Construction-Types (BCTs), enhances Emfrp by introducing recursive data types with size annotations yet the improved language keeps the static property mentioned above. In this paper, we formalize Emfrp extended with BCTs, present the algorithm for statically computing the runtime memory bounds, and prove its soundness.