Abstract for:
Paul B. Jackson. Nuprl and its use in circuit Design. In R.T. Boute,
V. Stavridou, T.F.Melham,editors, Proceedings of the 1992 Interational
Conference on Theorem Provers in Circuit Design , IFIP Transactions
A-10. North-Holland, 1992.
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.
Paul Jackson / jackson@cs.cornell.edu