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.

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.

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.

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/cpl

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.pdf

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=6

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/ptq