Presented at ITP 2017 - Interactive Theorem Proving.
Gabrielli A., Maggesi M. (2017)
Formalizing Basic Quaternionic Analysis.
In: Ayala-Rincón M., Muñoz C. (eds) Interactive Theorem
Proving. ITP 2017.
Lecture Notes in Computer Science, vol 10499. Springer, Cham.
@Inbook{Gabrielli_Maggesi_ITP2017, author = "Gabrielli, Andrea and Maggesi, Marco", editor = "Ayala-Rinc{\'o}n, Mauricio and Mu{\~{n}}oz, C{\'e}sar A.", title = "Formalizing Basic Quaternionic Analysis", bookTitle = "Interactive Theorem Proving: 8th International Conference, ITP 2017, Bras{\'i}lia, Brazil, September 26--29, 2017, Proceedings", year = "2017", publisher = "Springer International Publishing", address = "Cham", pages = "225--240", abstract = "We present a computer formalization of quaternions in the HOL Light theorem prover. We give an introduction to our library for potential users and we discuss some implementation choices.", isbn = "978-3-319-66107-0", doi = "10.1007/978-3-319-66107-0_15", url = "https://doi.org/10.1007/978-3-319-66107-0_15" }