I am investigating the theory of programming languages and using this theory to show various language systems and programs correct. Correctness of software and hardware is a difficult problem. Recent and repeated failures of carefully-developed and tested systems such as the telephone network have emphasized its importance and difficulty. Most software and increasingly large amounts of hardware are written in high-level programming languages, which—if the compilers are correct—automatically provide some forms of security (e.g. preventing type errors) and support for powerful reasoning principles (e.g. formal validation techniques). Establishing correctness—of compilers, languages, programs, and logics—must rely on accurate and formal specifications of programming languages. The field of semantics has a reputation for concentrating on finding ever better descriptions of languages, but having little impact outside the semantics community. My past and intended work is an example of the impact that semantics can and should have on the rest of computer science.
The semantic technique that I have found most useful is structured operational semantics (SOS), a discipline in which the behavior of a composite process as an abstract automaton is defined in terms of the behaviors of its component processes. This approach allows most of the reasoning principles of more abstract forms of semantics and thus is a suitable vehicle for proofs. Equally importantly, it uses only relatively straightforward structures and is thus suitable as a means of communicating with researchers who are not immediately interested in the frequently obscure mathematics of more abstract semantics. This is quite important in verifying compilers and logics: the language must be defined clearly as well as precisely, so that non-semanticists will agree that we are verifying with respect to the correct language.
Specifically, I am involved in projects in verifying silicon compilers and developing logics for concurrent real-time programs. I am also investigating the foundations of SOS semantics; I recently showed how to extract a complete equational reasoning system for any process algebra defined by SOS.
If you have questions or comments please contact: email@example.com.