| 2022 | ISAIM | A Formal Proof of the Banach-Tarski Theorem in ACL2(r). | Jagadish Bapanapally, Ruben Gamboa |
| 2022 | ITP | A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). | Jagadish Bapanapally, Ruben Gamboa |
| 2019 | VR | Visual Design Problem-based Learning in a Virtual Environment Improves Computational Thinking and Programming Knowledge. | Amy Banic, Ruben Gamboa |
| 2013 | SIGCSE | A more formal approach to "computer science: principles". | Rex L. Page, Ruben Gamboa |
| 2012 | ITP | A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. | Ruben Gamboa, John R. Cowles |
| 2011 | ITP | Automatic Differentiation in ACL2. | Peter Reid, Ruben Gamboa |
| 2010 | ITP | Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. | John R. Cowles, Ruben Gamboa |
| 2008 | ISSTA | Extending dynamic constraint detection with disjunctive constraints. | Nadya Kuzmina, John Paul, Ruben Gamboa, James L. Caldwell |
| 2006 | OOPSLA | Dynamic constraint detection for polymorphic behavior. | Nadya Kuzmina, Ruben Gamboa |
| 2004 | IDEAS | Curve-Based Representation of Moving Object Trajectories. | Byunggu Yu, Seon Ho Kim, Thomas Bailey, Ruben Gamboa |
| 2002 | FMCAD | Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem. | Jun Sawada, Ruben Gamboa |
| 1990 | EDBT | Abstract Machine for LDL. | Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy |
| 1989 | VLDB | Towards on Open Architecture for LDL. | Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy |