Publications

Book Chapters

  • “ACL2.” In The Seventeen Provers of the World, Wiedijk, Lecture Notes in Artificial Intelligence, 2006.
  • “Continuity and Differentiability in ACL2.” In Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Press, 2000.
  • “Inventory Control,” with D. Chimenti. In A Logical Language for Data and Knowledge Bases, Naqvi and Tsur, Computer Science Press, 1989.
  • “Resource Allocation and Deallocation,” with D. Chimenti. In A Logical Language for Data and Knowledge Bases, Naqvi and Tsur, Computer Science Press, 1989.

Edited Volumes

  • Hunt, W. and R. Gamboa (Eds.) Festschrift in Honor of Robert S. Boyer and J S. Moore. Future volume of Lecture Notes in Computer Science (LNCS).
  • Klein, G. and R. Gamboa (Eds.) Upcoming special issue of the Journal of Automated Reasoning.
  • Klein, G. and R. Gamboa (Eds.) Proceedings of 5th International Conference on Interactive Theorem Proving (ITP), Vienna, Austria, 2014.  Lecture Notes in Computer Science (LNCS), Vol. 8558.
  • Gamboa, R. and J. Davis (Eds.) Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications, Laramie, WY, 2013. Electronic Proceedings in Theoretical Computer Science (EPTCS), Vol. 114.
  • Gamboa, R., J. Cowles, and J. Sawada (Eds.) Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications, Austin, TX, 2007. Electronic Proceedings in the ACM Digital Library.

Refereed Journals

Refereed Conferences

Technical Reports

Talks and Presentations

  • “Gaming to Learn Computational Thinking,” with J. Leonard and J. Johnson. Presented at Texas Computer Education Association Annual Convention (TCEA), Austin, TX, 2015.
  • “On Vickrey’s Theorem and the Use of ACL2 for Formal Reasoning in Economics (Extended Abstract),” with J. Cowles. Presented at the 12th International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 2014.
  • “Amateur Astronomy.” Presented at the Launch Pad Workshop for writers of science fiction, Laramie, WY, 2012 and 2014.
  • “Distributed Architecture for Storing Non-Relational Data.” Presented at the International Conference on Information Technologies (ICIT), Saratov, Russia, 2012.
  • “ACL2(r): Got Reals?” Invited presentation at the 10th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, TX, 2011.
  • “Tales from the Front: How to Survive as a Software Entrepreneur.” Invited talk at the University of Oklahoma Center for the Creation of Economic Wealth (CCEW) Speaker Series, Normal, OK, 2010.
  • “Recent Models for Distributed and Multicore Programming.” Invited presentation at the Morningstar North American Tech Conference, Chicago, IL, 2010.
  • “Reasoning About DrScheme Programs in ACL2,” with M. Wiederrecht and C. MacLellan.  Presented at the 11th Symposium on Trends in Functional Programming (TFP), Norman, OK, 2010.
  • “A Mechanical Verification of Vitali’s Theorem in an Unlikely Logic.” Invited presentation at the University of Oklahoma, Norman, OK, 2010.
  • “An Entrepreneur’s Education from the School of Hard Knocks,” Keynote presentation at the e2e Laramie event, Laramie, WY, 2010.  Also presented at the StartWest summer meeting, Sheridan, WY, 2010.
  • “Enumerating Rationals without Repetitions,” with J. Caldwell and J. Cowles. Presented in ACL2 Workshop, Boston, 2009.
  • “Computing in Astronomy.” Presented at the Launch Pad Workshop for writers of science fiction, Laramie, WY, 2008,  2009, and 2011.
  • “The Chain Rule and Friends in ACL2(r).” Presented at the ACL2 Workshop, November 2007.
  • “Red-Black Trees for DrACuLa.” Presented at the ACL2 Workshop, November 2007.
  • “Dynamic Constraint Detection for Polymorphic Behavior” (poster), with N. Kuzmina. Presented in OOPSLA, Portland, 2006.
  • “Designing Spatio-Temporal Portals to Continuously Changing Network Nodes,” In Encyclopedia of Portal Technology and Applications, 2006.
  • “Mechanical Verification of Elementary Calculus Theorems in ACL2.” Presented at the Department of Mathematics of the University of Northern Colorado, September 2006.
  • “An Overview of Automated Reasoning.” Guest lecture in Diana Spears’ Artificial Intelligence II class, January 2006.
  • “Building Truly Database-Independent Applications.” Presented in Software Developer West (SD West), March 2005.
  • “Proving Elementary Calculus Theorems in ACL2,” Presented at Texas A&M University, College Station, TX, 1999.

Leave a Reply