Formal specification of image processing primitives in a functional language
I. Poole, Derek Charleston · 2002
Demonstrates that the primitive types and operations of an image processing library can usefully be specified in a general purpose functional programming language, even though they are implemented via an efficient representation in a procedural language. Theorems about the primitives can also be recorded within the functional languages. Thus it becomes possible to develop applications and reason formally about them within a single notation, from the image pixel level upwards.