This thesis demonstrates a correct, scalable and automated method to infer

semantic concepts using lattice-based ontologies, given relatively few manual

annotations. Semantic concepts and their relationships are formalized as a

lattice, and relationships within and between program elements are expressed as

a set of constraints. Our inference engine automatically infers concepts

wherever they are not explicitly specified. Our approach is general, in that

our framework is agnostic to the semantic meaning of the ontologies that it

uses.

Where practical use-cases and principled theory exist, we provide for the

expression of infinite ontologies and ontology compositions. We also show

how these features can be used to express of value-parametrized concepts and

structured data types. In order to help find the source of errors, we also

present a novel approach to debugging by showing simplified errors paths.

These are minimal subsets of the constraints that fail to type-check, and are

much more useful than previous approaches in finding the cause of program bugs.

We also present examples of how this analysis tool can be used to express

analyses of abstract interpretation; physical dimensions and units; constant

propagation; and checks of the monotonicity of expressions.