Ruben Gamboa - RankMe

44 papers A* 2A 1B 7C 1Misc 1Journal 5Unranked 21

Year	Rank	Type	Title / Venue / Authors
2025	—	`ed.`	Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, 12-13 May, 2025. ACL2 Ruben Gamboa, Panagiotis Manolios
2023	—	`conf`	Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses. ACL2 Ruben Gamboa, Panagiotis Manolios, Eric Whitman Smith, Kyle Thompson
2022	B	`conf`	A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). ITP Jagadish Bapanapally, Ruben Gamboa
2022	Misc	`conf`	A Formal Proof of the Banach-Tarski Theorem in ACL2(r). ISAIM Jagadish Bapanapally, Ruben Gamboa
2022	—	`conf`	A Free Group of Rotations of Rank 2. ACL2 Jagadish Bapanapally, Ruben Gamboa
2022	—	`conf`	All Prime Numbers Have Primitive Roots. ACL2 Ruben Gamboa, Woodrow Gamboa
2022	—	`conf`	Using ACL2 To Teach Students About Software Testing. ACL2 Ruben Gamboa, Alicia Thoney
2020	—	`ed.`	Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020. ACL2 Grant O. Passmore, Ruben Gamboa
2020	—	`conf`	Quadratic Extensions in ACL2. ACL2 Ruben Gamboa, John R. Cowles, Woodrow Gamboa
2019	A*	`conf`	Visual Design Problem-based Learning in a Virtual Environment Improves Computational Thinking and Programming Knowledge. VR Amy Banic, Ruben Gamboa
2018	—	`conf`	The Fundamental Theorem of Algebra in ACL2. ACL2 Ruben Gamboa, John R. Cowles
2017	—	`ch.`	Teacher Transformations in Developing Computational Thinking: Gaming and Robotics Use in After-School Settings. Emerging Research, Practice, and Policy on Computational Thinking Alan Buss, Ruben Gamboa
2017	—	`conf`	The Cayley-Dickson Construction in ACL2. ACL2 John R. Cowles, Ruben Gamboa
2016	J	`jnl`	Interactive Theorem Proving - Preface of the Special Issue. J. Autom. Reason. Gerwin Klein, Ruben Gamboa
2015	—	`conf`	Perfect Numbers in ACL2. ACL2 John R. Cowles, Ruben Gamboa
2014	—	`conf`	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis. ACL2 John R. Cowles, Ruben Gamboa
2014	—	`conf`	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent. ACL2 Ruben Gamboa, John R. Cowles
2014	B	`ed.`	Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings ITP Gerwin Klein, Ruben Gamboa
2013	A	`conf`	A more formal approach to "computer science: principles". SIGCSE Rex L. Page, Ruben Gamboa
2013	—	`conf`	An Interpreter for Quantum Circuits ACL2 Lucas Helms, Ruben Gamboa
2013	—	`ed.`	Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013. ACL2 Ruben Gamboa, Jared Davis
2012	B	`conf`	A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. ITP Ruben Gamboa, John R. Cowles
2012	—	`conf`	How Computers Work: Computational Thinking for Everyone TFPIE Rex L. Page, Ruben Gamboa
2011	B	`conf`	Automatic Differentiation in ACL2. ITP Peter Reid, Ruben Gamboa
2011	—	`conf`	Implementing an Automatic Differentiator in ACL2 ACL2 Peter Reid, Ruben Gamboa
2011	—	`conf`	Verifying Sierpinski and Riesel Numbers in ACL2 ACL2 John R. Cowles, Ruben Gamboa
2010	B	`conf`	Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. ITP John R. Cowles, Ruben Gamboa
2008	—	`conf`	Extending dynamic constraint detection with disjunctive constraints. WODA Nadya Kuzmina, John Paul, Ruben Gamboa, James L. Caldwell
2007	—	`conf`	Extending Dynamic Constraint Detection with Polymorphic Analysis. WODA@ICSE Nadya Kuzmina, Ruben Gamboa
2007	—	`ch.`	Spatio-Temporal Portals for Continuously Changing Network Nodes. Encyclopedia of Portal Technologies and Applications Byunggu Yu, Ruben Gamboa
2007	J	`jnl`	Theory Extension in ACL2(r). J. Autom. Reason. Ruben Gamboa, John R. Cowles
2006	—	`ch.`	ACL2. The Seventeen Provers of the World Ruben Gamboa
2006	—	`conf`	Dynamic constraint detection for polymorphic behavior. OOPSLA Companion Nadya Kuzmina, Ruben Gamboa
2006	—	`conf`	Implementing a cost-aware evaluator for ACL2 expressions. ACL2 Ruben Gamboa, John R. Cowles
2006	—	`conf`	Unique factorization in ACL2: Euclidean domains. ACL2 John R. Cowles, Ruben Gamboa
2004	—	`conf`	A Mechanical Proof of the Cook-Levin Theorem. TPHOLs Ruben Gamboa, John R. Cowles
2004	C	`conf`	Curve-Based Representation of Moving Object Trajectories. IDEAS Byunggu Yu, Seon Ho Kim, Thomas Bailey, Ruben Gamboa
2002	B	`conf`	Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem. FMCAD Jun Sawada, Ruben Gamboa
2002	J	`jnl`	The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2. Formal Methods Syst. Des. Ruben Gamboa
2001	J	`jnl`	Nonstandard Analysis in ACL2. J. Autom. Reason. Ruben Gamboa, Matt Kaufmann
1998	—	`conf`	Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2. IPPS/SPDP Workshops Ruben Gamboa
1990	B	`conf`	Abstract Machine for LDL. EDBT Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy
1990	J	`jnl`	The LDL System Prototype. IEEE Trans. Knowl. Data Eng. Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy, Shamim A. Naqvi, Shalom Tsur, Carlo Zaniolo
1989	A*	`conf`	Towards on Open Architecture for LDL. VLDB Danette Chimenti, Ruben Gamboa, Ravi Krishnamurthy