ask others

Jose Divasón

> Home > Persons

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

2010 – today

see FAQ

What is the meaning of the colors in the publication lists?

2018
[d9]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonJTY18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonJTY18
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified LLL algorithm. Archive of Formal Proofs 2018 (2018)
[d8]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonJTY18a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonJTY18a
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified factorization algorithm for integer polynomials with polynomial complexity. Archive of Formal Proofs 2018 (2018)
[c8]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/aisc/DivasonA18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/aisc/DivasonA18
Jose Divasón, Jesús Aransay:
A Formal Proof of the Computation of Hermite Normal Form in a General Setting. AISC 2018: 37-53
[c7]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/DivasonJKT018
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/DivasonJKT018
Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). CPP 2018: 2-13
[c6]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/iticse/RomeroD18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/iticse/RomeroD18
Ana Romero, Jose Divasón:
Experiences and new alternatives for teaching formal verification of Java programs. ITiCSE 2018: 383
[c5]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/DivasonJT018
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/DivasonJT018
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Formalization of the LLL Basis Reduction Algorithm. ITP 2018: 160-177
2017
[j3]
- view
  - electronic edition via DOI
  - electronic edition @ wikidata.org
- export record
  dblp key:
  - journals/jar/AransayD17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/AransayD17
Jesús Aransay, Jose Divasón:
A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem. J. Autom. Reasoning 58(4): 509-535 (2017)
[c4]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/DivasonJT017
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/DivasonJT017
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP 2017: 17-29
2016
[d7]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonJTY16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonJTY16
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
The Factorization Algorithm of Berlekamp and Zassenhaus. Archive of Formal Proofs 2016 (2016)
[d6]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonKTY16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonKTY16
Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Perron-Frobenius Theorem for Spectral Radius Analysis. Archive of Formal Proofs 2016 (2016)
[j2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/fac/AransayD16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/fac/AransayD16
Jesús Aransay, Jose Divasón:
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. Formal Asp. Comput. 28(6): 1005-1026 (2016)
2015
[d5]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonA15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonA15
Jose Divasón, Jesús Aransay:
QR Decomposition. Archive of Formal Proofs 2015 (2015)
[d4]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonA15a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonA15a
Jose Divasón, Jesús Aransay:
Echelon Form. Archive of Formal Proofs 2015 (2015)
[d3]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonA15b
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonA15b
Jose Divasón, Jesús Aransay:
Hermite Normal Form. Archive of Formal Proofs 2015 (2015)
[j1]
- view
  - electronic edition via DOI
  - electronic edition @ wikidata.org
- export record
  dblp key:
  - journals/jfp/AransayD15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jfp/AransayD15
Jesús Aransay, Jose Divasón:
Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm. J. Funct. Program. 25 (2015)
[c3]
- view
  - electronic edition via DOI
  - electronic edition @ wikidata.org
- export record
  dblp key:
  - conf/nfm/AransayD15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/nfm/AransayD15
Jesús Aransay, Jose Divasón:
Generalizing a Mathematical Analysis Library in Isabelle/HOL. NFM 2015: 415-421
2014
[d2]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonA14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonA14
Jose Divasón, Jesús Aransay:
Gauss-Jordan Algorithm and Its Applications. Archive of Formal Proofs 2014 (2014)
[c2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/aisc/Aransay-AzofraDHLPRR14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/aisc/Aransay-AzofraDHLPRR14
Jesús Aransay-Azofra, Jose Divasón, Jónathan Heras, Laureano Lambán, María Vico Pascual, Angel Luis Rubio, Julio Rubio:
Obtaining an ACL2 Specification from an Isabelle/HOL Theory. AISC 2014: 49-63
[i1]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/AransayD14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/AransayD14
Jesús Aransay, Jose Divasón:
Applications of the Gauss-Jordan algorithm, done right. CoRR abs/1401.5910 (2014)
2013
[d1]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/DivasonA13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/DivasonA13
Jose Divasón, Jesús Aransay:
Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs 2013 (2013)
[c1]
- view
  - electronic edition via DOI
  - electronic edition @ wikidata.org
- export record
  dblp key:
  - conf/lopstr/AransayD13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lopstr/AransayD13
Jesús Aransay, Jose Divasón:
Formalization and Execution of Linear Algebra: From Theorems to Algorithms. LOPSTR 2013: 1-18

Coauthor Index

see FAQ

maintained by

, founded at