Engineering foundations for software-driven systems.

Our lives are greatly influenced by software. Software enables nearly magical system behaviors and efficiencies, but sometimes it also behaves in ways that harm us, our society, our environment. The most essential role of any engineer is to *harness the magic* while also protecting the public from harm.

My aim as a researcher in software engineering is to find, test, and eventually promulgate fundamentally better ways for designers and engineers to succeed in these tasks.

CS6501: Special Topics in Software Engineering

If you're looking for information on the graduate course I'm teaching this semester, you're in the right place. Here you go.

Description: This is a special topics course in software engineering. The idea we will explore is that we can leverage ongoing advances in the formalization of abstract mathematics in type theory to provide new leverage for engineering software for systems in domains with complex mathematical underpinnings. Such domains include physics and the full range of cyber-physical systems. Along the way, you'll learn logic and proof construction, foundations of programming languages, advanced functional programming (with a Haskell-like syntax), some abstract mathematics, and more. By the end you will know how to use cutting-edge tools, namely type theory and modern proof assistants, to formalize abstract mathematical structures and theories, to enable new breakthroughs in the software engineering of cyber-physical and other complex (e.g., AI/DL) systems.

My academic activities

I'm on the faculty in Computer Science at the University of Virginia. There I conduct research with doctoral and other students, and teach both graduate and undergraduate students, and provide services to school and field. I enjoy teaching both undergraduate and graduate students. Because so much in our field depends on the ability to think abstractly, and because so few of our software professionals have sufficiently developed this intellectual capability, my main aim in teaching is for students to gain this skill. Too many computer science programs are satisfied to teach students to think in the concrete, procedural languages of industrial programming. I endeavor to complement these important skills with the ability to think in the declarative terms of higher-order mathematical logical languages of specification, verification, and the formalization of abstract mathematics. In research I've covered many areas, but an overriding theme has been on a combination of raising levels of abstraction but also making such abstractions composable. Work in this area has ranged from early work on modularization and real options to current efforts related to Daniel Jackson's idea of concepts as fundamental building blocks of highly usable software. Much of this work leverages our use of the constructive logic of the Lean proof assistant to formalize complex mathamtical and user interaction concepts. One particular project aims to formalize the abstract mathematics of physics as a semantic domain of software for many cyber-physical systems.

I am able to consult in numerous areas of software and systems engineering. Contact me privately for more information.

Interested in working with me?

Have you always wanted a PhD in computer science (and get paid to get it), with a particular interest in the role of mathematical thinking in advancing our ability to develop great systems? Give me a call.