Technical Report Number
The Edinburgh Logical Framework (LF) has been proposed as a system for expressing inductively deﬁned sets. I will present an inductive deﬁnition of the set of manifold meshes in LF. This deﬁnition takes into account the topological characteri-zation of meshes, namely their Euler Characteristic. I will then present a set of dependent data types based on this inductive def-inition. These data types are deﬁned in a programming language based on LF. The language’s type checking guarantees that any typeable expression represents a correct manifold mesh. Furthermore, any mesh can be represented using these data types. Hence, the encoding is sound and complete.
Brandt, Joel R., "What A Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms" Report Number: WUCSE-2005-15 (2005). All Computer Science and Engineering Research.