Ruben Gamboa

According to our database, Ruben Gamboa authored at least 41 papers between 1989 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses.

Ruben Gamboa, Panagiotis Manolios, Eric Whitman Smith, Kyle Thompson

Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, 2023

2022

A Free Group of Rotations of Rank 2.

Jagadish Bapanapally, Ruben Gamboa

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

Using ACL2 To Teach Students About Software Testing.

Ruben Gamboa, Alicia Thoney

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

All Prime Numbers Have Primitive Roots.

Ruben Gamboa, Woodrow Gamboa

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R).

Jagadish Bapanapally, Ruben Gamboa

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

A Formal Proof of the Banach-Tarski Theorem in ACL2(r).

Jagadish Bapanapally, Ruben Gamboa

Proceedings of the International Symposium on Artificial Intelligence and Mathematics 2022 (ISAIM 2022), 2022

2020

Quadratic Extensions in ACL2.

Ruben Gamboa, John R. Cowles, Woodrow Gamboa

Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, 2020

2019

Visual Design Problem-based Learning in a Virtual Environment Improves Computational Thinking and Programming Knowledge.

Amy Banic, Ruben Gamboa

Proceedings of the IEEE Conference on Virtual Reality and 3D User Interfaces, 2019

2018

The Fundamental Theorem of Algebra in ACL2.

Ruben Gamboa, John R. Cowles

Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, 2018

2017

The Cayley-Dickson Construction in ACL2.

John R. Cowles, Ruben Gamboa

Proceedings of the Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, 2017

Teacher Transformations in Developing Computational Thinking: Gaming and Robotics Use in After-School Settings.

Alan Buss, Ruben Gamboa

Proceedings of the Emerging Research, Practice, and Policy on Computational Thinking., 2017

2016

Interactive Theorem Proving - Preface of the Special Issue.

Gerwin Klein, Ruben Gamboa

J. Autom. Reason., 2016

2015

Perfect Numbers in ACL2.

John R. Cowles, Ruben Gamboa

Proceedings of the Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, 2015

2014

Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent.

Ruben Gamboa, John R. Cowles

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis.

John R. Cowles, Ruben Gamboa

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

2013

An Interpreter for Quantum Circuits

Lucas Helms, Ruben Gamboa

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

A more formal approach to "computer science: principles".

Rex L. Page, Ruben Gamboa

Proceedings of the 44th ACM Technical Symposium on Computer Science Education, 2013

2012

How Computers Work: Computational Thinking for Everyone

Rex L. Page, Ruben Gamboa

Proceedings of the Proceedings First International Workshop on Trends in Functional Programming in Education, 2012

A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers.

Ruben Gamboa, John R. Cowles

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Implementing an Automatic Differentiator in ACL2

Peter Reid, Ruben Gamboa

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

Verifying Sierpinski and Riesel Numbers in ACL2

John R. Cowles, Ruben Gamboa

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

Automatic Differentiation in ACL2.

Peter Reid, Ruben Gamboa

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure.

John R. Cowles, Ruben Gamboa

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

A Formalization of Powerlist Algebra in ACL2.

Ruben A. Gamboa

J. Autom. Reason., 2009

2008

Extending dynamic constraint detection with disjunctive constraints.

Nadya Kuzmina, John Paul, Ruben Gamboa, James L. Caldwell

Proceedings of the 2008 International Workshop on Dynamic Analysis: held in conjunction with the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2008), 2008

2007

Spatio-Temporal Portals for Continuously Changing Network Nodes.

Byunggu Yu, Ruben Gamboa

Proceedings of the Encyclopedia of Portal Technologies and Applications (2 Volumes), 2007

Theory Extension in ACL2(r).

Ruben Gamboa, John R. Cowles

J. Autom. Reason., 2007

Extending Dynamic Constraint Detection with Polymorphic Analysis.

Nadya Kuzmina, Ruben Gamboa

Proceedings of the Fifth International Workshop on Dynamic Analysis, 2007

2006

ACL2.

Ruben Gamboa

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

Dynamic constraint detection for polymorphic behavior.

Nadya Kuzmina, Ruben Gamboa

Proceedings of the Companion to the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2006

Implementing a cost-aware evaluator for ACL2 expressions.

Ruben Gamboa, John R. Cowles

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

Unique factorization in ACL2: Euclidean domains.

John R. Cowles, Ruben Gamboa

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

2004

A Mechanical Proof of the Cook-Levin Theorem.

Ruben Gamboa, John R. Cowles

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Curve-Based Representation of Moving Object Trajectories.

Byunggu Yu, Seon Ho Kim, Thomas Bailey, Ruben Gamboa

Proceedings of the 8th International Database Engineering and Applications Symposium (IDEAS 2004), 2004

2002

The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2.

Ruben Gamboa

Formal Methods Syst. Des., 2002

Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem.

Jun Sawada, Ruben Gamboa

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

2001

Nonstandard Analysis in ACL2.

Ruben Gamboa, Matt Kaufmann

J. Autom. Reason., 2001

1998

Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2.

Ruben Gamboa

Proceedings of the Parallel and Distributed Processing, 10 IPPS/SPDP'98 Workshops Held in Conjunction with the 12th International Parallel Processing Symposium and 9th Symposium on Parallel and Distributed Processing, Orlando, Florida, USA, March 30, 1998

1990

The LDL System Prototype.

Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy, Shamim A. Naqvi, Shalom Tsur, Carlo Zaniolo

IEEE Trans. Knowl. Data Eng., 1990

Abstract Machine for LDL.

Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy

Proceedings of the Advances in Database Technology, 1990

1989

Towards on Open Architecture for LDL.

Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy

Proceedings of the Fifteenth International Conference on Very Large Data Bases, 1989