http:^^www.cs.cornell.edu^info^people^jackson^papers^tp-in-cd-abstract.html

来自「This data set contains WWW-pages collect」· HTML 代码 · 共 38 行

MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 24-Nov-96 19:07:17 GMT
Content-Type: text/html
Content-Length: 1466
Last-Modified: Friday, 20-Jan-95 17:46:20 GMT

<title>Abstract of Nuprl and Circuit Design, TPCD92 Paper</title>
Abstract for:<br>
Paul B. Jackson. Nuprl and its use in circuit Design. In R.T. Boute, 
V. Stavridou, T.F.Melham,editors, <cite>Proceedings of the 1992 Interational 
Conference on Theorem Provers in Circuit Design </cite>, IFIP Transactions
A-10. North-Holland, 1992.
<p>
<hr>
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.
<i>Tactics</i> provide a high-level extendible toolkit for proof
development, while the soundness of the system relies only a fixed set
of rules.
<p>
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.

<hr>
Last Modified Jan 20th, 1995<p>

<address> Paul Jackson / <a href="mailto:[e-mail]">[e-mail]</a> </address>