Section Navigation

Johann receives National Science Foundation grant for computer science research

BOONE—A National Science Foundation grant totaling $377,083 has been awarded to Professor Patricia Johann in Appalachian State University’s Department of Computer Science.

View larger image

The three-year award will fund Johann’s research in an area of computational science called relational parametricity. Relational parametricity is a key technique computer scientists use to prove that computer programs are correct, or do what they are intended to do, Johann explained.

Johann has published extensively on relational parametricity and is considered a world expert on the subject. Her research interests include the mathematical foundations of computing. She has been working in the area of theoretical computer science for nearly 25 years and on relational parametricity for nearly 15 with computer scientists. She will carry out this research in collaboration with researchers from Glasgow, Edinburgh, and Copenhagen.

She began her research on the particular aspect of relational parametricity that is the focus of the NSF grant while at the University of Strathclyde in Glasgow, Scotland, where she was a professor of computer science.

“Relational parametricity is a way to express that the behavior of programs is uniform – that programs work in the same way on all their arguments, regardless of the types of those arguments,” Johann explained. “This uniformity allows us to deduce various important properties of our programs that can be useful both theoretically and practically. For example, relational parametricity is a key technique for proving that programs are correct, i.e., that programs do what they are intended to do.”

Johann is the principal investigator on the grant that will allow her to further develop the theory of relational parametricity.

Johann takes an approach to relational parametricity that is based on the categorical semantics of programming languages, meaning that they focus on what the constructs of programming languages mean, rather than how they are written.

“Categorical” means that they give their programing languages meaning by using a branch of mathematics known as category theory, which highlights mathematical structure.

Funds from the grant will provide two months of research salary for Johann and her student researchers during three summers, and support research visits with collaborators.