Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Awardee:APPALACHIAN STATE UNIVERSITY
Doing Business As Name:Appalachian State University
PD/PI:
  • Patricia Johann
  • (828) 262-7008
  • johannp@appstate.edu
Award Date:06/13/2014
Estimated Total Award Amount: $ 377,083
Funds Obligated to Date: $ 450,474
  • FY 2015=$73,391
  • FY 2014=$377,083
Start Date:09/15/2014
End Date:08/31/2018
Transaction Type:Grant
Agency:NSF
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:SHF: Small: Relational Parametricity for Program Verification
Federal Award ID Number:1420175
DUNS ID:781866264
Parent DUNS ID:066299918
Program:SOFTWARE & HARDWARE FOUNDATION
Program Officer:
  • Anindya Banerjee
  • (703) 292-8910
  • abanerje@nsf.gov

Awardee Location

Street:P.O. Box 32174
City:Boone
State:NC
ZIP:28608-2174
County:Boone
Country:US
Awardee Cong. District:05

Primary Place of Performance

Organization Name:Appalachian State University
Street:287 Rivers St.
City:Boone
State:NC
ZIP:28608-2068
County:Boone
Country:US
Cong. District:05

Abstract at Time of Award

Title: SHF: Small: Relational Parametricity for Program Verification The software market is currently estimated at $500 billion per year, and this figure is likely to grow significantly in real terms as software becomes ever more ubiquitous. One crucial aspect of software is that it be correct, i.e., that software does what's intended and does not go wrong. Even failures of everyday devices like iPods and mobile phones are inconvenient and frustrating, but software leaking credit card details or voting records, causing an airplane to crash, launching nuclear weapons without authorization, or compromising the global financial sector can lead to unprecedented and clearly unacceptable global uncertainties. The ever-growing size and sophistication of programs makes formal verification methods --- which use mathematical techniques to ensure that programs actually perform the computations they are designed to carry out and do not perform unintended ones --- increasingly critical for building truly secure and reliable software. The broader impact of this research is to make possible the development of better and more widely applicable formal program verification methods, and, thereby, to help ensure that even large and sophisticated software systems are provably correct. Relational parametricity is a key technique for formally verifying properties of software systems. Logical relations, upon which relational parametricity is based, provide a means of proving properties of a software system directly from the system itself. Logical relations have by now been developed for core fragments of many modern programming languages and verification systems. However, this has been accomplished by way of an enormous constellation of complicated and non-reusable logical relations, rather than by appealing to their uniform construction and transferrable development from fundamental principles. This research aims to improve the current state-of-the-art by providing an axiomatic framework for the construction of logical relations. The framework is principled, conceptually simple, comprehensive, uniform, and predictive. The intellectual merit of this research lies in its exposition and use of essential structures from category theory ("fibrations") to address the significant technical problems of constructing logical relations, and conceptualizing relational parametricity in sophisticated settings. It also lies in the novel and uniform formulation of parametricity to which this research will lead, and the application of this new framework to specific state-of-the-art computational problems. To ensure its uptake, a logic and tool support for the new framework will be provided. While the tool will permit users to experiment with the framework, the feedback from their practical experiences will further fortify the new foundations for parametricity.

Publications Produced as a Result of this Research

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

Kristina Sojakova Patricia Johann "A General Framework for Relational Parametricity" Juried Conference Paper, v., 2018, p.. doi:10.1145/3209108.3209141 


Project Outcomes Report

Disclaimer

This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.

In this project we corrected a rather large technical problem with a framework previously thought to guarantee type-uniformity in polymorphic programming languages. We discovered the problem with the existing framework, corrected it, showed that the corrected theory has as a direct instance type-uniformity for the language for which it was originally developed nearly 50 years ago, and showed that the corrected theory also extends to higher dimensions (and thus to languages supporting very sophisticated forms of type-uniformity). Showing that the corrected theory is also extensible to languages supporting more "real-world" features, such as algebraic effects, is ongoing work. Our framework for type-uniformity is a true framework, in the sense that it is developed once but used over and over again in different computational settings. For settings that are instances, our framework ensures that programs claiming to be type-uniform really do operate independently of their types, gives well-defined computational and mathematical meanings to algebraic data types, derives programming idioms and program transformations that can improve the performance of programs and be integrated into optimizing compilers, and provides strong correctness guarantees for programs that improve program verification.

On the non-technical side, this project brought the first-ever post-doctoral researchers, and the first world-class research, to a primarily undergraduate department at a regional state university. It also involved an undergraduate researcher in some coding in support of the project.


Last Modified: 10/07/2018
Modified by: Patricia Johann

For specific questions or comments about this information including the NSF Project Outcomes Report, contact us.