Add to ORKGThe purpose of this thesis is twofold: (1) to define a formal lattice-theoretic calculus of partially ordered type structures where the ordering is meant to reflect subtyping; (2) to propose a model of computation which amounts to solving systems of simultaneous equations in a lattice of types. The specific contributions which I believe to be original of the research presented here are: (1) An extrapolation of the syntactic properties of first-order terms to provide insight in formalizing record-like type structures; (2) A simple type-as-set semantics and a motivational discussion of what this entails for the operational use of partially ordered types in programming; (3) A lattice-theoretic calculus of type subsumption and a formal univer...