Software has become critical to nearly every aspect of our civilization.  Consequently, the complexity of our tools and our needs for dependability have increased immensely. Programmers need scalable tools and methodologies to keep complexity in check. Generic programming, with roots in computer algebra and symbolic mathematics, is one of the promising approaches to scalable and dependable software construction. This talk presents the design and implementation of a system for axiomatic programming and its application to mathematical software construction. Key novelties include direct support for user-defined axioms establishing local type equalities and overload resolution based on equational theories and local  axioms. I will illustrate uses of axioms and their organization into concepts to support generic programming as practiced in computational mathematical systems.

 Short bio:

Dr. Gabriel Dos Reis is an assistant professor in the Department of Computer Science and Engineering at Texas A&M University.  He received his PhD in Mathematics from Université Paris-VII and École Normale Supérieure de Cachan, France. His research interests include mathematical software, applied formal methods, programming languages and libraries, and generic programming. Dr. Dos Reis received a prestigious NSF Career award in 2012 for his research in compilers for dependable computational mathematics. He is an active member of  the ISO C++ standards committee where he currently chairs the C++ standards Study Group on undefined behavior. He authored and co-authored several features of the 2011 ISO C++ standards. He leads the Liz project, a platform for research into axiomatic programming. He served as Release Manager of GCC, the GNU Compiler Collection.