What a Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms
Published in Washington University in St. Louis, 2005
Programming language approach to representing meshes, The Edinburgh Logical Framework (LF) has been proposed as a system forexpressing inductively defined sets. I will present an inductive definition of the set of manifold meshes in LF. This definition takes into account the topological characterizationof meshes, namely their Euler Characteristic.I will then present a set of dependent data types based on this inductive definition.These data types are defined in a programming language based on LF. Thelanguage’s type checking guarantees that any typeable expression represents a correctmanifold mesh. Furthermore, any mesh can be represented using these data types.Hence, the encoding is sound and complete., Meshes, formal language theory, proofs, https://openscholarship.wustl.edu/cse_research/932/, 52
authors: Joel Brandt
Authors: Joel Brandt
Download Paper