Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #533 | |
|---|---|
| Title: | Extracting Circuits from Constructive Proofs |
| Authors: | Basin,D |
| Date: | May 1991 |
| Presented: | In the Proceedings of ACM 1991 International Workshop on Formal Methods in VLSI Design |
| Keywords: | |
| Abstract: | We lay a foundation for using constructive type theory as a tool for combining hardware synthesis and verification. Specifically, we specialize the proofs-as-programs paradigm for the Nuprl constructive type theory to "proofs-as-circuits", whereby representations of circuits can be automatically synthesized from constructive proofs. We use a limited form of syntactic reflection to guarantee that synthesized objects correspond to circuits; the soundness of the type theory guarantees that these objects meet their stated behavioral specifications. our approach allows the modular construction of combinational and parameterized combinational circuits in parallel with their proofs of correctness. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}