Dependable Data Structures by Dependent Types

依赖类型的可靠数据结构

• 批准号: 22700004
• 负责人: HAMANA Makoto
• 金额: $ 2.5万
• 依托单位: Gunma University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22700004/
• 关键词: データ構造; 情報基礎; 自動定理証明; 関数プログラム; 依存型; 情報学基礎

Dependent types are data types which ensure more precise properties of data thanordinary data types. Using dependent types, we develop a theory and applications ofdependable data structures, aiming to establish foundations of reliable computer softwares.

依赖类型是一种数据类型，它比普通数据类型确保了更精确的数据属性。利用依赖类型，我们发展了可靠数据结构的理论和应用，旨在为可靠的计算机软件奠定基础。

项目成果

Dependent Polynomial Functors for Inductive Families

归纳族的相关多项式函子

• 发表时间: 2011

Another Initial Algebra Semantics of Inductive Families for Programming

用于编程的归纳族的另一种初始代数语义

• 发表时间: 2010
• 作者: Y. Hu;H. Hashimoto;S. Imahori;M. Yagiura;M.Hamana
• 通讯作者: M.Hamana

Constructing Correct Looping Arrows from Cyclic Terms : Traced Categorical Interpretation in Haskell

从循环项构建正确的循环箭头：Haskell 中的追踪分类解释

• 发表时间: 2012
• 作者: Shoji Noguchi;Yoshiko Kosugi;Makoto Tani;Satoru Takanashi;Abd Rahman Lassim;Siti Aisah Shamsuddin;M. Hamana
• 通讯作者: M. Hamana

Semantic Labelling for Proving Termination of Combinatory Reduction Systems, Functional and Constraint Logic Programming, Lecture Notes in Computer Science

用于证明组合约简系统终止的语义标签、函数和约束逻辑编程、计算机科学讲义

• 发表时间: 2010
• 期刊: Springer-Verlag
• 作者: 中島 隆;大野充昭;園山 亘;笈田育尚;Emilio S.Hara;前川賢治;窪木拓男;佐々木淳一,松本卓也,江草 宏,矢谷博文,今里 聡;M. Hamana
• 通讯作者: M. Hamana

チューリングを読む-コンピュータサイエンスの金字塔を楽しもう

阅读图灵 - 享受计算机科学的不朽著作

• 发表时间: 2012
• 作者: チャールズ・ペゾルド (著);井田哲雄;鈴木大郎;奥居哲;浜名誠;山田俊行 (訳)
• 通讯作者: 山田俊行 (訳)