PRL Seminars

Aleksey Nogin


The Status of the Meta-Prl Project


October 4, 1999


Comment

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

Slides

slides
Home