Self introduction
2007 年 慶應義塾大学大学院政策・メディア研究科修士課程了。 電機メーカの研究部門にて
形式手法、ソフトウェアテストなどのソフトウェア高信頼化の研究に従事した後、現在は Preferred Networks, Inc. にてエンジニアとして働く。 関数型プログラミングや理論計算機科学に興味を持つ。 訳書(共訳)に『抽象によるソフトウェア設計−Alloyではじめる形式手法−』、『型システム入門−プログラミング言語と型の理論−』。
Work experience
-
株式会社Preferred Networks
Engineer
2017-05 -
-
東芝
研究者
I worked as a researcher for System Engineering Laboratory, Toshiba Research and Development Center. I have worked in software dependability team to develop technology based on formal methods, program analysis, automatic test-case generation to achieve more dependable systems. I have also worked in cities infrastructure solutions team and developed a recommendation system that recommends brick-and-mortar shops/goods on smart-phone for regional promotion.
* Recommendation system for Kawasaki Grand City Mall project
* SMT-based semi-automatic test-case generation for FBD (Function Block Diagram) programs for power plant control systems
* Specification mining based on UNSAT core enumeration
* Helping language/runtime design of “Molatomium”, a parallel programming model for “Cell Broadband Engine”-like heterogeneous multicore processors
* CForge: Bounded model checker for C language
* Verification of work-flow networks based on model checking2007-04 - 2017-04
Projects
-
Ruby-GNOME2
Ruby-GNOME2 is a set of Ruby language bindings for the GNOME >=2.0 development environment. I was one of core developers in the early days. In particular I have designed/wrote a general bridge between Ruby's object system and GObject object system using reflection/introspection features and replaced non-extensible hard-coded one in its predecessor Ruby/GTK1.
2016-4 - 2016-4
-
PTQ : An implementation of Montague's PTQ in Haskell
Montague grammer and the PTQ (The Proper Treatment of Quantification in Ordinary English) by Richard Montague were pioneering work in the field of formal semantics of natural languages, and showed that natural languages (like English) and formal languages (like programming languages) can be treated in the similar way. I implemented his theory in interactive environment.
http://hackage.haskell.org/package/PTQ
https://github.com/msakai/ptq2016-4 - 2016-4
-
CPL : A categorical programming language interpreter
I implemented an interpreter of CPL, a functional programming language based on category theory, designed by Prof. Tatsuya Hagino. In CPL, data types are declared in a categorical manner by adjunctions. Each data type is declared with its basic operations or morphisms. Programs consist of these morphisms, and execution of programs is the reduction of elements (i.e. special morphisms) to their canonical form.
http://hackage.haskell.org/package/CPL
https://github.com/msakai/cpl2016-4 - 2016-4
-
Economic load dispatch
Economic load dispatch is the determination of the output of electricity generation units, that meet the electricity demands with lowest possible cost, subject to complex operational constraints. I assisted research project of economic load dispatch problem by removing performance bottlenecks of our prototype optimization system, setting up continuous integration environment, and writing minor modules of the system. My work is partly applied to the system for TEPCO Fuel & Power, Incorporated.
http://www3.toshiba.co.jp/power/whatsnew/topics/20161026/index_j.htm
http://www.toshiba.co.jp/tech/review/2016/03/71_03pdf/0A.pdf#page=62015-11 - 2016-12
-
Kawasaki Grand City Mall
Toshiba carried a demonstration experiment on smart city and O2O service around Kawasaki Station (c.f. http://www.toshiba.co.jp/about/press/2013_12/pr_j1901.htm http://www.city.kawasaki.jp/200/page/0000053904.html (written in Japanese)). As part of this experiment, we have developed a recommendation system that recommends brick-and-mortar shops/goods on smart-phone for regional promotion. I leaded a team for data analysis and recommendation algorithm development.
2013-12 - 2015-10
-
toysolver / toysat
Solver implementation of various problems including SAT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic. In particular It contains a moderately-fast pure-Haskell SAT solver 'toysat'. I submitted it to solver competitions (Pseudo Boolean Competition and Max-SAT Evaluations) and ranked high in some competition categories.
2011-1 - 2016-4
-
CForge: Bounded model checker for C language.
CForge is a C program analyzer based on a program analysis framework Forge developed by the Software Design Group (SDG) at MIT, and we developed CForge as part of a joint research project with MIT SDG. I worked as a main developper of CForge, and worked on its overall design, design of our formal specification langauge for C, implementaion of a kind of C compiler, and so on.
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462652
http://www.toshiba.co.jp/tech/review/2009/08/64_08pdf/a06.pdf2007-4 - 2012-12
Links
What I'm good at
-
2数理計画
-
1モデル検査
-
1Mathematical Optimization
-
1Haskell
-
1Computer Science
-
1Continuous Integration
-
1継続的統合
-
1Alloy
-
0Machine Learning
-
0Python
-
0Java
-
0機械学習
-
0推薦システム
-
0Recommender systems
-
0Ruby
Education
-
Keio University
Graduate School of Media and Governance
2007
-
Keio University
Faculty of Policy Management
2005
-
Shonan High School
2000
Courses
-
慶應 萩野・服部研究室
2001-10 - 2007-3
Clubs/volunteering
-
圏論勉強会
Category theory is a highly general and abstract mathematical theory, which has applications not only in mathematics but also in theoretical computer science, functional programming, physics, linguistics and many other fields. I was one of core members of the study group and we had studied following materials:
* “Conceptual Mathematics: A First Introduction to Categories” by F. William Lawvere and Stephen Hoel Schanuel,
* “Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist” by Andrea Asperti and Giuseppe Longo,
* “The Haskell Programmer's Guide to the IO Monad -- Don't Panic” by Stefan Klinger,
* “Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics” by Samson Abramsky
* “A survey of graphical languages for monoidal categories” by Peter Selinger
* “Categorical Logic and Type Theory” by Bart Jacobs.
There is an Japanese article about this study group: “Technical Study Session Map in Japan - Join a Live Session of Engineers!”, 情報処理, Vol.52, No.4, Apr. 2011. http://id.nii.ac.jp/1001/00073853/2014-1 - 2012-12
-
RHG読書会
This study group was a group of programming language geeks. It was started initially as a study group of reading “Rubyソースコード完全解説” (known as “Ruby Hacking Guide”), but eventually we have studied many programming and programming language related books/materials:
* YARV (Ruby >=1.9 VM),
* なでしこ (a Japanese programming language),
* MinCaml,
* “ふつうのLinuxプログラミング--Linuxの仕組みから学べるgccプログラミングの王道”,
* “ふつうのHaskellプログラミング--ふつうのプログラマのための関数型言語入門”,
* “入門JavaScript”,
* “実践Common Lisp” (Japanese translation of “Practical Common Lisp”),
* “ふつうのコンパイラをつくろう--言語処理系をつくりながら学ぶコンパイルと実行環境の仕組み”.2003-1 - 2009-12
Languages
-
English
Professional
-
Japanese
Native
Publications
-
型システム入門―プログラミング言語と型の理論
2013-3
-
抽象によるソフトウェア設計 ―Alloyではじめる形式手法
2011-7
-
SAT問題と他の制約問題との相互発展
2015-1
-
MC/DC-like Structural Coverage Criteria for Function Block Diagrams
2014-3
-
Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定
2013-8
-
Model-checking C programs against JML-like specification language
2012-12
-
非正格関数に対して適用可能な融合変換
2007-1
Connections on Wantedly View all 18
-
Technical solution consultant, Android partner engineering / Google
-
Data Scientist / freee株式会社
-
技術顧問 / 株式会社ITMONO
-
フリーランスエンジニア / ぼのたけ(フリーランス)
-
サーバーサイドエンジニア / 株式会社Folio
-
Engineer/programmer / 東芝
Recommendations
No recommendations

- Connections on Wantedly 18
No connections

No connections

No recommendations

Wanted Score
120