Many scientific fields rely on high-performance computing in order to accurately simulate complex physical phenomena involving high dimensional tensors (multi-dimensional arrays). In particular, implementations of algorithms in the domain of computational quantum chemistry follow one of two paths: excruciatingly slow and error-prone expert hand-coding which results in very fast but inflexible code, or general, library-based (or code generation-based) development, which reduces development effort but often leaves significant performance on the table. The project's impact is to enable provably correct (correct by construction) code generation of key computational routines in a high-performance manner that can be incorporated into larger code bases. This contributes to the overall goal of whole-program verification of scientific applications. The project’s novelties are 1) new notations for describing operations involving structured matrices and tensors, 2) new insights to identify high-performance algorithms from their specification, and 3) integrating complex data movement into the specification of the algorithm to better identify and exploit optimization opportunities at various abstraction levels. Techniques and algorithms developed by the project will broadly impact the theory and practice of computational science, data science, and machine learning. All aspects of the work will involve the training of young scientists at the graduate and undergraduate student levels. T