During his two-week visit to the EMG group, Kohei aims at investigating
the relation between ODEs and WHILEdt. WHILEdt is an imperative language
extended with an "infinitesimal" constant. By using this language,
one can model hybrid systems in the form of imperative programs. This week Kohei designed a translation from ODE into
WHILEdt, and proved that this translation is correct if the
original ODE has a unique solution. In the next week, Kohei plans to investigate ODEs with non-unique solutions.
