\documentclass[
11pt,a4paper]{
article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\newcommand\isafor{
\textsf{IsaFoR}}
\newcommand\ceta{
\textsf{Ce
\kern-.
18emT
\kern-.
18emA}}
\begin{document}
\title{Executable Matrix Operations on Matrices of Arbitrary Dimensions}
\author{Christian Sternagel and Ren
\'e Thiemann}
\maketitle
\begin{
abstract}
We provide the operations of matrix addition, multiplication,
transposition, and matrix comparisons as executable functions over
ordered semirings. Moreover, it is proven that strongly normalizing (monotone) orders
can be lifted to strongly normalizing (monotone) orders over matrices.
We further show that the standard semirings over the naturals, integers, and
rationals, as well as the arctic semirings satisfy the axioms that are required
by our matrix theory.
Our formalization was performed as part of the
\isafor/
\ceta-system
\cite{CeTA}
\footnote{
\url{
http://cl-informatik.uibk.ac.at/software/ceta}}
which
contains several termination techniques. The provided theories have been
essential to formalize matrix-interpretations
\cite{MatrixJAR} and
arctic interpretations
\cite{Arctic}.
A short description of this formalization can be found in
\cite{WST10}.
\end{
abstract}
\tableofcontents
% include generated text of all theories
\input{session}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
