@misc{imm-21-aa-descr,
  title = {Affine Arithmetic},
  author = {Fabian Immler},
  year = 2021,
  month = dec,
  url = {https://www.isa-afp.org/browser_info/current/AFP/Affine_Arithmetic/document.pdf},
  howpublished = {Online dicument},
  comment = {Detailed description of AA with extra ops and algorithms. Intersection with a hyperplane.},
  abstract = {We give a formalization of affine forms [1, 2] as abstract representations of zonotopes. We provide affine operations as well as overapproximations of some non-affine operations like multiplication and division. Expressions involving those operations can automatically be turned into (executable) functions approximating the original expression in affine arithmetic. Moreover we give a verified implementation of a functional algorithm to compute the intersection of a zonotope with a hyperplane, as described in the paper [3].}
}