A partial implementation of an abstract notation provides an implementation for some of the notations operations on some of the values in the notation. A collection of partial implementations of a fixed notation -differing in the selection of values and operations implemented- caters to different patterns of usage of the notation in individual programs. Partial implementations of a general mathematical notation are more appropriate to the formal development of programs than the more familiar paradigm of abstract data types with complete implementations. Furthermore, partial implementations provide the only realistic account of the implementation of finite machinery of many familiar mathematical notations. From a practical point of view, partial implementations of a fixed notation exhibit great reusability and provide a convenient approach to early prototyping in program development. The incorporation of mathematical notations into a programming system is studied, with particular regard to the formal development of programs in the style of Dijkstra and Gries. A new notion of encapsulation is presented to define partial implementations and a predicate-transformer characterization of implementation correctness is defined. The implementation correctness criterion simplifies and extends the original data-type implementation criterion of Hoare, generalizes implementation criterion for algebraic abstract data types, and accommodates the implementation of non-deterministic operations. Different variables of the same type may have different representations and implementations of operations within the same program. Not all implementations are adequate in a given program, so syntactic and semantic conditions are given to ensure that a proposed implementation of a variable is adequate.