Introduction -- Nature of the PRL Project

Project Focus

The project remains focused on logic-based tools to support programming and on implementing formal computational mathematics; we see these as inextricably linked activities. Over the years the scope of the project has expanded - from developing individual programs and theorems to constructing systems and theories. Starting with the slogan "proofs-as-programs," we now talk about "theories-as-systems." This change of scale has led to a new class of problems and challenges discussed throughout this project summary.


We are currently focused on these goals:

More details on project goals »

Technical Content and Cross Links

The project is multi-faceted. One way to understand it is to see its projections onto other areas of computer science and mathematics. The standard projections are onto these topics: