Output details

Meadows and the equational specification of division

<11> Division 1/x is a partial operation because it is not continuous at 0. This is the first algebraic theory of total division in which 1/0=0, a convention in software tools (e.g., in verification by Harrison (Intel)). The new notion of meadow solves problems beyond the scope of classical field theory: it specifies division using equations; it classifies embeddings into affine spaces. The paper led to 9 further papers. For example, safe error recovery methods for meadows are used by Burgess to study system rollback in operating systems (J Logic Algebraic Programming 80 (2011) 427–443).