Skip to main content
PRL Project

The Status of the Meta-Prl Project

by Aleksey Nogin

In this talk I will attempt to describe what MetaPRL can do for those
who are willing to try to use it. In particular, I will describe new
features (compared to Nuprl 4) that MetaPRL has:
- Speed
- Clean and modular code base
- Derived rules
- Modular theories mechanism
- Rewrites and conditional rewrites
- Extended proof browsing/editing
- Resource annotations
- Transparent concurrent and distributed refinement
- Multiconclusion sequents