ATS言語を使って不変条件をAPIに強制する

• Item type: Symposium(1)
• 公開日: 2015-01-09
• タイトル: ATS言語を使って不変条件をAPIに強制する
• タイトル / 言語: en
• タイトル: Invariant captured by ATS's API
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: ATS，関数型言語，依存型，線形型，組込開発
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: METASEPI DESIGN
• 著者所属(英): en
• 著者所属(英): METASEPI DESIGN
• 著者名: 岡部, 究
• 著者名(英): Kiwamu, Okabe
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 「モノのインターネット」という概念が提唱されています。バスケットボールのような、なんの変哲もないモノがインターネットに接続されるようになるでしょう。そのような機器は複雑な機能を持つ一方、現代の組み込み機器はC言語を用いて開発されており、不具合を誘発する危険性がつきまとっています。本論文ではこの問題に対する1つの解決策としてATS言語を紹介します。このATS言語はMLのような関数型言語で、静的な強い型を持ちます。また依存型を持ち、証明器としても機能します。さらにこの言語の線形型を使うことで、メモリやロックのようなリソースの制御を安全に行なうことができます。ATSコンパイラはC言語を経由して実行バイナリを生成するため、強い型による不変条件の強制は常にソースコードと同期しています。最後にわずか8kBのメモリしか持たないArduinoボード上でATS言語を使って設計したアプリケーションを動作させ、組み込み領域にATS言語を適用可能であることを示します。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: ``Internet of Things''; simple object such like basketball will be connected to the Internet. On the one hand such product should have many features, on the other various embedded system are designed with C language today. The C language code is possible to crash with various issues. In this paper, I introduce ATS language to address this issue. ATS language is a functional language such like ML, and has statically strong type system. It has dependent types and linear types that are used to manage memory resource and lock safely. The invariant captured by ATS's strong type is constantly synchronous the source code, because ATS compiler produces execution binary via C language. Finally, I show an ATS language application running on the Arduino board that only has 8kB SRAM, to proof that we can use ATS language for embedded system.
• 書誌情報: 夏のプログラミング・シンポジウム2014「ビューティフル・インターフェイス」報告集; 巻 2014, p. 1-8, 発行日 2015-01-09
• 出版者 / 言語: ja
• 出版者: 情報処理学会