The goal of the Plato project is to develop software engineering tools
and techniques that help modern programmers create more reliable and secure
component software systems. In order to accomplish our goal, we
are developing a system of logical type refinements (LTR) that
conservatively extend type systems for modern programming languages like
Java, C# and ML.
LTR guarantee properties of programs as they
are written, linked together, executed and evolve through all aspects
of the software lifecycle. More specifically, we are developing
LTR that allow programmers to specify a rich of collection of domain-specific
- the contents of component data structures,
- the ordering and effect of operations specified
in an interface,
- the safety of components acquired from different
- the distribution of data and computations
over a network.
LTR are specified in a concise notation familiar
to programmers. In addition, sophisticated refinement checking and
refinement inference techniques allow programmers to minimize the number
of annotations they need to put on their programs.
Plato Walker, Philosopher Canine pub
Robert Harper and Members of the Triple
Internet Programming Home