Programming Languages & Methodologies
In the area of programming languages and methodology, we are interested in the design, implementation and use of programming languages, and in the methods and mathematics of program construction. Effective programming in all areas of computer science and in all applications requires good language design, reliable and efficient implementation and good programming methods. Our department has a history of innovation in this area, including the influential Euclid project on verifiable programming, the SP/k teaching subsets of PL/1, variable precision constructs and exception handling for numerical computation and the Turing language currently in use in many schools.
Our research includes the integration of Turing and an advanced programming environment for the management of software architectures (component relationships). We are also developing an algebra of software architectures. In cooperation with others, we are designing and implementing data-parallel language features. Also in cooperation with the IBM Toronto research lab, we are implementing highly-optimizing and parallel compilers, and investigating how they can be used to simplify the design of hardware while improving performance.
On the theoretical side, we are also interested in the logical foundation of programming. We have developed a programming logic that enables us to describe computations using a single boolean expression, and express the programming refinement order as ordinary implication. It applies to both terminating and nonterminating computation, to sequential and parallel computation, to stand-alone and interactive computation. In the future, this may have a practical benefit: a programming system that can report logic errors in programs just as it now reports syntax errors. Some initial investigations suggest that the programming logic may be as good for deriving VLSI circuits as for deriving programs.