PhD, University of California, San Diego
BA, Mathematics, Stanford University
Professor, University of Oklahoma
Director and Professor, University of Oklahoma
Reseach Leader, Amoco
Professor, Colorado State University
Engineering reliable software, logic-based testing and verification, applications of mechanized logic, functional programming
Rex Page focuses on methods for the design and development of reliable digital circuits and software. He observes that digital circuits and software comprise formulas in mathematical logic, which brings the full force of mathematical analysis to bear on the design of such systems through applications of formal logic supported by tools like proof assistants and model checkers that facilitate complex analytics and mechanize details. Mechanized logic may, in fact, be the only feasible route to the engineering of circuits and software with fully understood behavior.
Since widespread use of the tools of mechanized logic cannot take place until a significant portion of practitioners appreciate the benefits of such tools and know how to use them, Dr Page advocates significant experience with applied logic in the baccalaureate studies of all students in computer science and software engineering. Accordingly Dr Page, in collaboration with researchers from other universities, has developed educational material providing such exposure in a form that can be used in three courses required in 90% of undergraduate computing education programs. His current efforts are devoted to expanding, improving, and promoting applied logic education in undergraduate computer science and software engineering programs.
Dr Page has been working in the area of reliable software for over three decades, both in academia and industry. His early work developed effective software engineering methods for massively parallel computing systems. Dr Page believes that procedural programming is a monumental waste of human energy.
AWARDS, HONORS AND PROFESSIONAL ACTIVITIES
Program Chair, Trends in Functional Programming, 2010.
Program Committee, Eighth International Workshop On The ACL2 Theorem Prover and Its Applications.
Program Committee, Implementation and Application of Functional Languages, 2010.
Reviewer, IEEE Transactions on Computers.
Engineering software correctness, Journal of Functional Programming 17, 6 (Nov 2007) 675-686
Software is discrete mathematics, Proceedings of the Eighth International Conference on Functional Programming, Uppsala, Sweden (August 25-27, 2003) 79-86
Functional Programming and Theor em Proving for Undergraduates: A Progress Report FDPE 2008, Victoria, B.C., Canada (Sep 21, 2008) 21-29 (with Carl Eastlund and Matthias Felleisen)
ACL2 in DrScheme, Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, Seattle Washington (Aug 15-16, 2006) 107-116 (with Dale Vaillancourt and Matthias Felleisen)
Experience with a large scientific application in a functional language, Conferenceon Functional Programming Languages and Computer Architecture, Copenhagen (June 1993) ACM Press, 3-1 (with Brian Moe)