浜名 誠

J-GLOBALへ         更新日: 18/09/20 19:27
 
アバター
研究者氏名
浜名 誠
 
ハマナ マコト
eメール
hamanacs.gunma-u.ac.jp
URL
http://www.cs.gunma-u.ac.jp/~hamana/
所属
群馬大学大学院
部署
理工学府 電子情報部門
職名
准教授
学位
博士(工学)(筑波大学)

プロフィール

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

研究分野

 
 

経歴

 
2018年3月
 - 
現在
群馬大学 大学院理工学府 電子情報部門 准教授
 
2014年4月
 - 
2018年2月
群馬大学 大学院理工学府 電子情報部門 助教
 
2013年4月
 - 
2014年3月
群馬大学 大学院理工学研究院 電子情報部門 助教
 
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)  プログラム委員長
 

受賞

 
2018年9月
日本ソフトウェア科学会 第35回大会 優秀発表賞 関数プログラム・計算系の分割停止性検証: 外山-Klop-Barendregt の定理の高階化
 
https://jssst2018.wordpress.com/
2018年5月
FLOPS 2018 Best paper award "Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation"
 
http://www.sqlab.jp/FLOPS2018/
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

論文

 
Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation
浜名 誠
14th International Symposium on Functional and Logic Programming (FLOPS 2018),   Lecture Notes in Computer Scie 99-115   2018年5月   [査読有り]
T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp J. Nagele, N. Nishida, K. Shintani, and H. Zankl
the Leibniz International Proceedings in Informatics (LIPIcs)   108 32:1-32:5   2018年7月   [査読有り]
We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.
浜名 誠
Mathematical Structures in Computer Science   28(2) 287-337   2018年   [査読有り]
How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories and Computation
浜名 誠
Proceedings of the ACM on Programming Languages   1(22) 1-28   2017年9月   [査読有り]
We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool SOL, Second-Order Laboratory, which as...
A Functional Implementation of Function-as-Constructor Higher-Order Unification
浜名 誠
Proc. International Workshop on Unification (UNIF'17)   1-6   2017年9月   [査読有り]
Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories
浜名 誠
Logical Methods in Computer Science   13(8) 1-38   2017年   [査読有り]
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月   [査読有り]
M. Hamana
Electronic Proceedings in Theoretical Computer Science   (191) 75-89   2015年9月   [査読有り]
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年   [査読有り]
M. Hamana
Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science   6604 381-395   2011年
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年   [査読有り]
Makoto Hamana
Higher-Order and Symbolic Computation, Springer Science+Business Media   19(2/3)    2006年   [査読有り]
Makoto, Neil Ghani, Tarmo Uustalu
Higher-Order and Symbolic Computation, Springer Science+Business Media   19(2/3) 263-282   2006年   [査読有り]

書籍等出版物

 
チャールズ・ペゾルド (担当:共訳)
日経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年       代表者: 浜名 誠