| A mechanized proof of the Basic Perturbation Lemma J Aransay, C Ballarin, J Rubio Journal of Automated Reasoning 40 (4), 271-292, 2008 | 47 | 2008 |
| Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm J Aransay, J Divason Journal of Functional Programming 25, e9, 2015 | 17 | 2015 |
| Generating certified code from formal proofs: a case study in homological algebra J Aransay, C Ballarin, J Rubio Formal Aspects of Computing 22 (2), 193-213, 2010 | 16 | 2010 |
| Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL J Aransay, J Divasón Formal Aspects of Computing 28, 1005-1026, 2016 | 15 | 2016 |
| Formalization and execution of Linear Algebra: from theorems to algorithms J Aransay, J Divasón Logic-Based Program Synthesis and Transformation: 23rd International …, 2014 | 12 | 2014 |
| A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem J Aransay, J Divasón Journal of Automated Reasoning 58 (4), 509-535, 2017 | 9 | 2017 |
| Four approaches to automated reasoning with differential algebraic structures J Aransay, C Ballarin, J Rubio Artificial Intelligence and Symbolic Computation: 7th International …, 2004 | 9 | 2004 |
| Generalizing a mathematical analysis library in Isabelle/HOL J Aransay, J Divasón NASA Formal Methods Symposium, 415-421, 2015 | 8 | 2015 |
| Towards a higher reasoning level in formalized Homological Algebra J Aransay½, C Ballarin¾, J Rubio½ CALCULEMUS-2003, 84, 2003 | 7 | 2003 |
| Enseñanza de Sistemas de Información Geográfica (SIG) en estudios de grado y posgrado en la Universidad de La Rioja: principios teóricos y ejercicios prácticos MS Andrades Rodríguez, JM Aransay Azofra, MP Diago Santamaría, ... | 6 | 2020 |
| The Isabelle/HOL Algebra Library J Aransay, C Ballarin, M Baillon, PE de Vilhena, S Hohe, F Kammüller, ... Technical report, Isabelle Library, University of Cambridge Computer …, 2019 | 6 | 2019 |
| Gauss-Jordan algorithm and its applications J Divasón, J Aransay Archive of Formal Proofs, 2014 | 5 | 2014 |
| Rank-nullity theorem in linear algebra J Divasón, J Aransay Archive of Formal Proofs, 2013 | 5 | 2013 |
| A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and ACL2 J Aransay, J Divasón, J Heras, L Lambán, P Pascual, AL Rubio, J Rubio Technical report, 2012. http://wiki. portal. chalmers. se/cse/uploads …, 2012 | 5 | 2012 |
| Modelling differential structures in proof assistants: the graded case J Aransay, C Domínguez International Conference on Computer Aided Systems Theory, 203-210, 2009 | 5 | 2009 |
| Extracting computer algebra programs from statements J Aransay, C Ballarin, J Rubio Computer Aided Systems Theory–EUROCAST 2005: 10th International Conference …, 2005 | 5 | 2005 |
| QR Decomposition. Archive of Formal Proofs, 2015 J Divasón, J Aransay | 5 | |
| Fin de un viaje infinito: integración continua para prácticas de programación J Aransay, J Heras Asociación de Enseñantes Universitarios de la Informática (AENUI), 2020 | 4 | 2020 |
| Análisis del uso de datos geográficos y sistemas de información geográfica en las enseñanzas de grado y master de una universidad MS Andrades, J Aransay, JÁ Llorente, MP Diago, E Sáenz de Cabezón, ... Asociación de Enseñantes Universitarios de la Informática (AENUI), 2018 | 4 | 2018 |
| Performance Analysis of a Verified Linear Algebra Program in SML J ús Aransay, J Divasón | 4 | 2013 |
Julio RubioUniversidad de La RiojaVerified email at unirioja.es
