レンズとモナドを用いた軽量線形型プログラミング

Imai Keigo; Garrigue Jacques

文献

J-GLOBAL ID：202002240159543770 整理番号：20A0553744

レンズとモナドを用いた軽量線形型プログラミング

Lightweight Linearly-typed Programming with Lenses and Monads

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手 {{ this.onShowCLink("http://jdream3.com/copy/?sid=JGLOBAL&noSystem=1&documentNoArray=20A0553744&COPY=1") }}
高度な検索・分析はJDreamⅢで {{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=20A0553744&from=J-GLOBAL&jstjournalNo=U0109A") }}

著者 (2件)： ,
資料名：
巻： 27 ページ： 431-444(J-STAGE) 発行年： 2019年
JST資料番号： U0109A ISSN： 1882-6652 資料種別：逐次刊行物 (A)
記事区分：原著論文発行国：日本 (JPN) 言語：英語 (EN)

本論文では,OCamlにおける線形型の符号化とその応用を示した。この符号化により,線形型により誘導する安全な資源アクセスに基づいて正しいOCamlプログラムを書き込むことができる。線形型は,全ての変数を正確に1回使用することを確実にし,これにより,静的方法における資源アクセスと通信プロトコルのようなプログラムの挙動的側面をチェックするために使用することができる。しかしながら,線形型は既存のプログラミング言語に統合するために著しい努力を必要とした。この符号化は,レンズとパラメータ化したモナドを用いることにより,バニラのOCaml型チェッカーが線形性を強化することを可能とした。パラメータ化したモナドは,事前および事後条件を有するモナドであり,それらを用いて,型レベルで資源の形成と消費を追跡した。データ型の一部に焦点を合わすレンズを用いて,事前および事後条件において資源を参照した。線形型リストのような快適に構造化されたデータを扱うために,さらに,OCamlの構文拡張機構に基づきパターンマッチングへの拡張を提案した。本論文では,OCmalにおいて通信プロトコルの静的チェックへの応用を示した。(翻訳著者抄録)

, , , , , , , , ,
, , , , ,

著者キーワード (5件)： , , , ,

システムプログラミング一般

引用文献 (29件)：

[1] Atkey, R.: Parameterized Notions of Computation, Journal of Functional Programming, Vol.19, No.3-4, pp.335-376 (online), DOI: 10.1017/S095679680900728X (2009).
[2] Ben-Ari, M.: How to solve the Santa Claus problem, Concurrency: Practice & Experience, Vol.10, No.6, pp.485-496 (online), DOI: 10.1002/(SICI)1096-9128(199805)10:6<485::AID-CPE329>3.0.CO;2-2 (1998).
[3] Benton, P.N.: A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models, Computer Science Logic, 8th International Workshop, LNCS, Vol.933, pp.121-135, Springer (online), DOI: 10.1007/BFb0022251 (1994).
[4] Bernardy, J.-P., Boespflug, M., Newton, R.R., Jones, S.P. and Spiwack, A.: Linear Haskell: Practical linearity in a higher-order polymorphic language, PACMPL, Vol.2, No.POPL, pp.5:1-5:29 (online), DOI: 10.1145/3158093 (2018).
[5] Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C. and Schmitt, A.: Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem, ACM Trans. Program. Lang. Syst., Vol.29, No.3, p.17 (online), DOI: 10.1145/1232420.1232424 (2007).

, , , ,

前のページに戻る