Current research projects

(As of 2010.)

My research interests include formal methods of programming software and hardware, specification languages, tools for formal program development, languages and compilers for hardware programming and hardware/software co-design, and program animation for teaching programming

See my publications page for papers.

Some of my current research projects are listed below

• The Teaching Machine. Progam animation means showing what's going on inside the computer as programs execute. The Teaching Machine is a program animator for C++ and Java. It is used in teaching these languages and for teaching programming concepts and data structures and algorithms. This project is a collaboration with Michael Bruce-Lockhart. Much of the programming was done by Derek Reilly. Some students who have contributed include John Anderson, Michael Burton, Shawn Cross, Stephen Hale, and Sun Hao. Other collaborators have included Yannis Cotronis and Pierluigi Crescenzi.
• HARPO. HARPO stands for HARdware Programming with Objects. HARPO/L is a programming language for hardware/software co-design. The language is based on the idea of a network of cooperating, multi-threaded objects. My students and I have been designing the language and investigating methods of compiling it and similar languages to programmable hardware such as Coarse-Grained Reconfigurable Architectures. Currently we are looking at methods of proving concurrent programs free of certain classes of error and that they meet their specifications. Some of the students who are working or have worked on this with me include Rani Gnanolivu, Ashraful Tuhin, Ken Zhang, Xiangwen Li, Lei Zhang, Yan Hao, and Shuang Wu.
  Here is a snapshot of the HARPO language, as of Dec 2010.
• Syntax and overview Language-Design-6.pdf
• Static semantics (a bit out of date) static-semantics-4a.pdf
• Dynamic semantics grainless-semantics.pdf
• SIMPLE. SIMPLE is a project to develop an editor and proof checker for program development. SIMPLE's wide spectrum language is based on a strongly and polymorphically typed version of Eric Hehner's 'Practical Theory of Programming' (aka Predicative Programming). Stephen Motty has been working on this with me.
• Predicative programming and generic algorithm development. General algorithmic approaches --such as binary search, divide and conquer, greediness, and dynamic programming-- can be formalized as generic algorithms and proved correct independently of any intended application. We can then specialize these algorithms to particular applications, and so reuse not only the algorithm, but also its proof. Leila Mofara worked on this project.

Past projects

• SMALL. SMALL is a low level synchronous language for programming hardware (especially FPGAs). My students Ying Shen and Wei Song collaborated on it with me.
• Robotics. Together with Ray Gosine and Siu O'Young, I supervised Faustina Hwang and Jamie King who were working on the coordination of multiple cooperating robots.
• Xanthine/Xylia. Xanthine and Xylia are two different attempts to produce an XML editing platform suitable as a user interface for the SIMPLE tool set. Xylia was a joint project with Dennis Peters. Some of the studen ts who worked on it were Pouria Shaker, Naeim Semsarilar, and John Milley. Xanthine is a more recent approach, based on simultaneously supporting W3C's DOM interface and Swing's Document interface. Xanthine and Xylia eventually gave way to a Mozilla-based XML editor called GEFN, which I am developing as the underlying platform for SIMPLE 's user-interface.