EAGER: Exploration in Type Systems With User-Defined Axioms

Texas A&M Engineering Experiment Station, College Station TX

Investigators

Abstract

The aim of this exploratory project is to conduct a study of practical programming with user-defined axiom to explore how semantic information, expressed through axioms, can be taken advantage of in structured generic programming. This work is a preliminary step to doing research on dependable, scalable generic programming, with application to scientific software. More specifically, the PI will investigate how, and which forms of user-defined axioms can be turned into property decision procedures that complement conventional type systems. This target of this work is the C++ programming language, which has a huge base of code and programmers and thus will have a broad impact. The work will address the question of how axioms can be used to make programs simpler, more flexible, and provide semantic information to code generators. The system will be released as open source software and evaluated on software from computer algebra.