@inproceedings{56ab923e05f8454cafb9c12e40e81e1a,
title = "Combining engineering vigor with mathematical rigor",
abstract = "Higher order logic and a functional language are used to document and verify design procedures which correctly synthesize array multipliers of arbitrary size. The procedures work with general negabinary inputs and create design descriptions corresponding to practical designs which are correct-by-construction.",
author = "Chin, {Shiu Kai}",
note = "Funding Information: §This work was partially supported by NSF Grant MIP-8710826, IBM Contract 845, and Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1990. Copyright: Copyright 2017 Elsevier B.V., All rights reserved.; Mathematical Sciences Institute Workshop on Hardware Specification, Verification and Synthesis, 1989 ; Conference date: 05-07-1989 Through 07-07-1989",
year = "1990",
doi = "10.1007/0-387-97226-9_28",
language = "English (US)",
isbn = "9780387972268",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "152--176",
editor = "Miriam Leeser and Geoffrey Brown",
booktitle = "Hardware Specification, Verification and Synthesis",
}