What A Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms

Authors

Joel R. Brandt, Washington University in St. Louis

Document Type

Technical Report

Publication Date

2005-04-15

Filename

WUCSE-2005-15.pdf

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.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7BC3WV7

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