著者

叢 悠悠

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.37, no.1, pp.1_84-1_85, 2020-01-24 (Released:2020-03-24)

著者

叢 悠悠 浅井 健一

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.36, no.2, pp.2_47-2_60, 2019-04-26 (Released:2019-06-25)

---

CoqやAgdaなどの定理証明支援系では,依存型を使ってプログラムの性質を正確に記述することができる.一方,依存型付き言語の多くは,副作用を許さないという制約もつ.これは,副作用の動的な振る舞いによって型が静的に定まらなくなることによるが,副作用の欠如は実用的なプログラムの実装の妨げとなるため,適切な制約を設けながら,依存型付き言語に副作用を導入する試みがなされてきた.本研究では,限定継続命令 shift/resetをもつ依存型付き言語を考える.shift/resetはさまざまな副作用の模倣を可能にするが,その応用例や型システムは単純型付き言語で考えられてきた.本稿では,shift/reset と依存型を組み合わせるために必要な制約を明らかにし,健全な型システムを定義する.また,設計した言語に対するCPS変換を与え,変換が型を保存することを証明する.

著者

山本 雄也 叢 悠悠 島村 龍太郎 菅野 幸夫 北原 鉄朗 糸山 克寿

雑誌

研究報告音楽情報科学(MUS) (ISSN:21888752)

巻号頁・発行日

vol.2022-MUS-133, no.7, pp.1, 2022-01-18

---

本稿では第 133 回音楽情報科学研究会における既発表の国際会議・萌芽・デモ・議論セッションの発表内容について述べる.本セッションでは, 査読付きジャーナルもしくは国際会議にて既発表の研究成果や,これからの発展が期待される萌芽的な研究まで,幅広くポスター発表・デモ・議論できる場である.今回のセッションでは,合計 4 件の発表が行われる.