MetaPRL presents a framework for formal algorithmic knowledge in the form of a Logical Programming Environment. MetaPRL users can use the framework for reasoning about programs, for automating the generation of new algorithms, and as a reference for formal algorithm development using the native interface and the Formal Digital Library. Knowledge in MetaPRL is organized as a set of modules, which correspond to components in the programming language. In MetaPRL, the programmer is provided with a set of tools that are integrated with the development environment to provide automated reasoning and program synthesis.
Knowlege in MetaPRL is organized as a set of libraries that start with the foundations for mathematics, and extend to knowledge for reasoning about very specific computational domains. The following theories represent the core MetaPRL contribution to the Formal Digital Library, presented bottom-up.