Document Type
Technical Report
Publication Date
2005-04-15
DOI:
10.7936/K7BC3WV7
Technical Report Number
WUCSE-2005-15
Abstract
The Edinburgh Logical Framework (LF) has been proposed as a system for expressing inductively defined sets. I will present an inductive definition of the set of manifold meshes in LF. This definition 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 defined 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.
Recommended Citation
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.
https://openscholarship.wustl.edu/cse_research/932
Comments
Permanent URL: http://dx.doi.org/10.7936/K7BC3WV7