10th Workshop on Computation: Theory and Practice (WCTP 2020)
開催地
和文:
英文:
アブストラクト
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.
各種検索
サポート
ヘルプ