Abstract
Nuprl is an interactive theorem proving system in the LCF tradition. It has a higher order logic and a very expressive type theory; the type theory includes dependent function types (Pi types), dependent product types (Sigma types) and set types. Nuprl also has a well developed X-Windows user interface and allows for the use of clear and concise notations, close to ones used in print. Proofs are objects which can be viewed, and serve as readable explanations of theorems. Tactics provide a high-level extendible toolkit for proof development, while the soundness of the system relies only a fixed set of rules.
We give an overview of the Nuprl system, focusing in particular on the advantages that the type theory brings to formal methods for circuit design. We also discuss ongoing projects in verifying floating-point circuits, verifying the correctness of hardware synthesis systems, and synthesizing circuits by exploiting the constructivity of Nuprl's logic.
We give an overview of the Nuprl system, focusing in particular on the advantages that the type theory brings to formal methods for circuit design. We also discuss ongoing projects in verifying floating-point circuits, verifying the correctness of hardware synthesis systems, and synthesizing circuits by exploiting the constructivity of Nuprl's logic.
| Original language | English |
|---|---|
| Title of host publication | Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings |
| Publisher | North-Holland Publishing Company |
| Pages | 311-336 |
| Number of pages | 26 |
| ISBN (Print) | 0-444-89686-4 |
| Publication status | Published - 1992 |