浜名 誠

J-GLOBALへ         更新日: 17/05/17 17:39
 
アバター
研究者氏名
浜名 誠
 
ハマナ マコト
eメール
hamanacs.gunma-u.ac.jp
URL
http://www.cs.gunma-u.ac.jp/~hamana/
所属
群馬大学大学院
部署
理工学府 電子情報部門
職名
助教

プロフィール

日本学術振興会特別研究員として京都大学、英国エジンバラ大学LFCSを経て、2001年から群馬大学助教。プログラムのための数学的構造を明らかにし、それをソフトウェアの構成へ役立てる事に興味があります。高階抽象構文、高階項書換え系、圏論、型理論を用いたプログラム基礎理論、意味論とその関数型プログラミング言語への応用を研究しています。2008年にソフトウェア科学会論文賞、2007年に高橋奨励賞を受賞。

研究分野

 
 

経歴

 
2014年4月
 - 
現在
群馬大学 大学院理工学府 電子情報部門 助教
 
2013年4月
 - 
2014年3月
群馬大学 大学院理工学研究院 電子情報部門 助教
 
2001年4月
 - 
現在
Gunma University Department of Computer Science Assistant Professor
 
2007年4月
 - 
2013年3月
群馬大学 大学院工学研究科 情報工学専攻 助教
 
2001年4月
 - 
2007年3月
群馬大学 工学部 情報工学科 助手
 
1999年4月
 - 
2001年2月
英国エジンバラ大学 計算機科学基礎研究所(LFCS) 客員研究員
 
1998年4月
 - 
2001年3月
日本学術振興会 受け入れ機関:京都大学情報学研究科  特別研究員PD
 

学歴

 
1993年4月
 - 
1998年3月
筑波大学 工学研究科 電子・情報工学専攻
 

委員歴

 
2017年4月
 - 
現在
日本ソフトウェア科学会  代表委員
 
2014年4月
 - 
現在
日本ソフトウェア科学会  プログラミング論研究会(PPL) 運営委員
 
2016年
 - 
現在
13th International Symposium on Functional and Logic Programming (FLOPS'16)  program committee member
 
2015年
 - 
現在
International Workshop on Fixed Points in Computer Science (FICS'15)  program committee member
 
2015年
   
 
第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015)  プログラム委員長
 

受賞

 
2016年3月
日本ソフトウェア科学会 第18回プログラミングおよびプログラミング言語ワークショップ 発表賞 プログラミング言語研究のための(高階)項書換え系入門
 
http://logic.cs.tsukuba.ac.jp/ppl2016/
2012年11月
群馬大学 横山科学技術賞 「依存型による安全で高信頼なソフトウェアの基礎研究」
 
2008年5月
日本ソフトウェア科学会 第12回 論文賞 「高階書換え系の停止性のための代数モデル」
 
http://www.jssst.or.jp/award/detail/ronbunsho_list.html
2007年6月
日本ソフトウェア科学会 第23回 高橋奨励賞 「Representing Cyclic Structures as Nested Datatypes」
 
http://www.jssst.or.jp/award/detail/takahashi_list.html

論文

 
Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories
浜名 誠
Logical Methods in Computer Science      2017年   [査読有り]
accepted. to appear.
Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theoryies
M. Hamana
The 1st International Conference on Formal Structures for Computation and Deduction (FSCD'16)      2016年4月   [査読有り]
Iteration Algebras for UnQL Graphs and Completeness for Bisimulation
M. Hamana
Electronic Proceedings in Theoretical Computer Science   (191) 75-89   2015年9月   [査読有り]
Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
Marcelo Fiore, Makoto Hamana
Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)   520-529   2013年7月   [査読有り]
We formalise and study the notion of polymorphic algebraic theory, as
understood in the mathematical vernacular as a theory presented by equations
between polymorphically-typed terms with both type and term variable binding.

The prototypical exam...
Makoto Hamana
Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science 7294   7294 136-150   2012年   [査読有り]
Polymorphic Abstract Syntax via Grothendieck Construction
M. Hamana
Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science   6604 381-395   2011年
A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach
Marcelo Fiore, Makoto Hamana
Proc. of 7th ACM SIGPLAN Workshop on Generic Programming (WGP 2011)   59-70   2011年   [査読有り]
M. Hamana
Functional and (Constraint) Logic Programm   5979 62-78   2010年   [査読有り]
補関数の生成による複製機能付きプログラムの自動双方向化
松田一孝, 胡振江, 中野圭介, 浜名誠, 武市正人
コンピュータソフトウェア   26(2) 56-75   2009年   [査読有り]
Makoto Hamana
Lecture Notes in Computer Science   5608 127-141   2009年
Makoto Hamana
Lecture Notes in Computer Science   5979 62-78   2009年   [査読有り]
Makoto Hamana
Proc. of Ninth ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'07)   97-108   2007年   [査読有り]
K. Matsuda, Z. Hu, K. Nakano, M. Hamana, M. Takeichi
Proc. of 12th ACM SIGPLAN International Conference on Functional Programming (ICFP'07)   42(9) 47-58   2007年   [査読有り]
An Initial Algebra Approach to Term Rewriting Systems with Variable Binders
Makoto Hamana
Higher-Order and Symbolic Computation, Springer Science+Business Media   19(2/3)    2006年   [査読有り]
Explicit Substitutions and Higher-Order Syntax
Makoto, Neil Ghani, Tarmo Uustalu
Higher-Order and Symbolic Computation, Springer Science+Business Media   19(2/3) 263-282   2006年   [査読有り]
Representing Cyclic Structures as Nested Datatypes
HAMANA MAKOTO / Neil Ghani / Tarmo Uustalu / Varmo Vene
Trends in Functional Programming   173-188   2006年   [査読有り]
浜名 誠
コンピュータソフトウェア   Vol. 23(No. 2) 142-156   2006年   [査読有り]
第12回日本ソフトウェア科学会論文賞論文。Klopによって提案された高階書換えの体系コンビナトリー簡約系 (Combinatory Reduction Systems, CRSs) がFiore,Plotkin,Turiらによる構文の代数モデルΣモノイドによって健全かつ完全にモデル化できることを示す.このモデルを整礎な推移的関係を持つものに制限すると,停止性を持つCRSの完全な特徴付けができる.このことを用いて,与えられたCRSの停止性を代数的な解釈によって示すという便利な手法を与える.
Universal Algebra for Termination of Higher-Order Rewriting
Makoto Hamana
Rewriting Techniques and Applications (RTA'05), Lecture Notes in Computer Science   3467 348-363   2005年   [査読有り]
Free Sigma-monoids: A Higher-order Syntax with Metavariables
Makoto Hamana
The Second Asian Symposium on Programming Languages and Systems (APLAS'04), Lecture Notes in Computer Science   3202 348-363   2004年   [査読有り]
Term Rewriting with Variable Binding: An Initial Algebra Approach
Makoto Hamana
Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2003), ACM Press   148-159   2003年   [査読有り]

書籍等出版物

 
チャールズ・ペゾルド (担当:共訳)
日経BP社   2012年6月   ISBN:4822283720
井田 哲雄, 浜名 誠 (担当:共著)
サイエンス社   2006年12月   ISBN:4781911358

担当経験のある科目

 

競争的資金等の研究課題

 
高階代数系指向プログラミングの原理―安全・柔軟なソフトウェアへ向けて
文部科学省: 科学研究費補助金(基盤研究(C))
研究期間: 2017年4月 - 2020年3月    代表者: 浜名 誠
依存型による安心・安全・高信頼ソフトウェアの基礎理論
稲盛財団研究助成金: 
研究期間: 2012年 - 2014年    代表者: 浜名 誠
文部科学省: 科学研究費補助金(挑戦的萌芽研究)
研究期間: 2013年4月 - 2016年3月    代表者: 浜名 誠
文部科学省: 科学研究費補助金(基盤研究(B))
研究期間: 2012年4月 - 2015年3月    代表者: 浜名 誠
依存型プログラミング言語による安全性の保証された木構造とポインタの操作ライブラリ
国立情報学研究所: 共同研究費 (共同研究者 胡 振江)
研究期間: 2009年       代表者: 浜名 誠
依存型を持つプログラミング言語を用いて、木データ構造とそれ上のポインタを操作する基本操作をライブラリを作成した。
循環共有構造のデータ型とその関数型プログラミング言語における実現
国立情報学研究所: 共同研究費 (共同研究者 龍田 真)
研究期間: 2007年       代表者: 浜名 誠
文部科学省: 科学研究費補助金(若手研究(B))
研究期間: 2004年 - 2006年    代表者: 浜名 誠
本年は、著書1本、学術論文誌3本の出版、国際会議論文1本の出版の成果を得た。著書「計算モデル論入門」はメタプログラミングシステムの基礎となる計算のための基礎理論を解説した入門書である。論文誌コンピュータソフトウェアVol.23で出版された論文「高階書換え系の停止性のための代数モデル」は、長く未解決だった高階書換えの体系コンビナトリー簡約系の完全な代数モデルを与えた。メタプログラミングシステムのための計算体系としてメタ書換えの完全な代数的な特徴付けを得た。論文誌Higher-Order an...
文部科学省: 科学研究費補助金(若手研究(B))
研究期間: 2007年 - 2009年    代表者: 浜名 誠
コンピュータ上での効率のよい計算に頻出する、サイクルと共有の構造を持つデータ構造を数理的構造を持つデータ型、すなわち再起データ型で表現する手法を探求し、関数型プログラミング技術への応用を行った。
文部科学省: 科学研究費補助金(若手研究(B))
研究期間: 2010年 - 2011年    代表者: 浜名 誠
本年は、依存型による安全性の保証があるデータ構造の表現と理論の解明を行った。まず、循環共有ポインタを持つ木構造のデータに対して安全な依存型の表現方法を明かにした。ここでの安全性とは、未確定領域を指すポインタがデータ構造上にないことを保証したものである。これを依存型プログラミング言語Agdaを用いて実装し、その有効性を示した。さらにこれを前層の圏における始代数として特徴づけすることに成功した。この結果は、学術論文誌Logical Methods in Computer Scienceにて出版...
束縛データ構造を持つ関数・論理プログラミング言語
大川情報通信基金: 研究助成金
研究期間: 2002年       代表者: 浜名 誠