|
EducationPh.D. (1977) Cornell University Research Area: Computational theory, computational algebra and logic, logics and semantics of programming languagesMy research interests include the theory of computational complexity, especially complexity of decision problems in logic and algebra, and program logic and semantics. In the past I have worked on algorithms for type inference in programming languages; static analysis of programs; functional decomposition of polynomials and rational and algebraic functions; and algorithms for resolution of singularities. My most recent interests include the theory and applications of Kleene algebra and Kleene algebra with tests (Kleene/Boolean algebra) in programming language semantics and verification. Selected PublicationsKleene algebra and bytecode verification (with Lucja Kot); in Proc. 1st Workshop Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode'05), (Fausto Spoto, ed.), Edinburgh, 2005, pp. 201–215. Coinductive proof principles for stochastic processes; in Proc. 21st Conf. Logic in Computer Science (LICS'06), IEEE, Seattle, WA, 2006. Relational semantics for higher-order programs (with Kamal Aboul-Hosn); in Proc. Mathematics of Program Construction (MPC'06), 2006. Automating proofs in category theory (with Christoph Kreitz and Eva Richter); in Proc. 3rd Int. Joint Conf. Automated Reasoning (IJCAR'06), Seattle, WA, 2006. KAT-ML: an interactive theorem prover for Kleene algebra with tests (with Kamal Aboul-Hosn), Journal of Applied Non-Classical Logics (2006). Local variable scoping and Kleene algebra with tests (with Kamal Aboul-Hosn); in Proc. 9th Int. Seminar on Relational Methods in Computer Science and 4th Int. Workshop Applications of Kleene Algebra (Kleene/RelMiCS'06), 2006. Theory of Computation, Springer, New York, 2006. Last modified: May 24, 2006 |