Jose Divasón
Jose Divasón
Verified email at unirioja.es - Homepage
Title
Cited by
Cited by
Year
A formalization of the Berlekamp-Zassenhaus factorization algorithm
J Divasón, S Joosten, R Thiemann, A Yamada
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017
172017
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, 2015
152015
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
J Aransay, J Divasón
Formal Aspects of Computing 28 (6), 1005-1026, 2016
132016
Formalization and execution of Linear Algebra: from theorems to algorithms
J Aransay, J Divasón
International Symposium on Logic-Based Program Synthesis and Transformation …, 2013
112013
and" GTA.
V Pascual, I Randen, K Thompson, M Sioud, JN Forre, D Capra
The Journal of Clinical Investigation 86 (4), 1323-1325, 1990
7*1990
A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm
J Divasón, SJC Joosten, R Thiemann, A Yamada
Journal of Automated Reasoning, 1-37, 2019
62019
Efficient certification of complexity proofs: Formalizing the Perron–Frobenius theorem (invited talk paper)
J Divasón, S Joosten, O Kunčar, R Thiemann, A Yamada
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
62018
Generalizing a mathematical analysis library in Isabelle/HOL
J Aransay, J Divasón
NASA Formal Methods Symposium, 415-421, 2015
62015
A formalization of the LLL basis reduction algorithm
J Divasón, S Joosten, R Thiemann, A Yamada
International Conference on Interactive Theorem Proving, 160-177, 2018
52018
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
52012
QR Decomposition. Archive of Formal Proofs, 2015
J Divasón, J Aransay
5
Performance Analysis of a Verified Linear Algebra Program in SML
J ús Aransay, J Divasón
42013
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
32017
Generating Persistence Structures for the Integration of Data and Control Aspects in Business Process Monitoring.
E Domínguez, B Pérez, ÁL Rubio, MA Zapata, A Allué, A López, ...
ICEIS (2), 320-327, 2018
22018
Perron–Frobenius theorem for spectral radius analysis
J Divasón, O Kuncar, R Thiemann, A Yamada
Archive of Formal Proofs, 2016
22016
Echelon form
J Divasón, J Aransay
Archive of Formal Proofs, 2016
22016
Hermite normal form
J Divasón, J Aransay
Archive of Formal Proofs, 2015
22015
Gauss-Jordan algorithm and its applications
J Divasón, J Aransay
Archive of Formal Proofs, Sept, 2014
22014
Rank-nullity theorem in linear algebra
J Divasón, J Aransay
Archive of Formal Proofs, 2013
22013
NOTA
M PASCUAL, A RUBIO, I PÉREZ, S NÁJERA
21988
The system can't perform the operation now. Try again later.
Articles 1–20