{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:34:39Z","timestamp":1725496479393},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668565"},{"type":"electronic","value":"9783540466741"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46674-6_14","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T15:50:17Z","timestamp":1196351417000},"page":"151-162","source":"Crossref","is-referenced-by-count":0,"title":["Logical Relations in Circuit Verification"],"prefix":"10.1007","author":[{"given":"Mia","family":"Indrika","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,19]]},"reference":[{"key":"14_CR1","volume-title":"Category Theory for Computing Science","author":"M. Barr","year":"1990","unstructured":"M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall International, London, 2nd edition, 1990.","edition":"2nd edition"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"C. Brown and G. Hutton. Categories, Allegories, and Circuit Design. In Proc. of 10th Annual IEEE symposium on Logic in Computer Science. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316052"},{"key":"14_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 6th International Conference Computer Aided Verification (CAV\u201994)","author":"J. Burch","year":"1994","unstructured":"J. Burch and D. Dill. Automated Verification of Pipelined Microprocessors Control. In Proc. of 6th International Conference Computer Aided Verification (CAV\u201994), volume 818 of LNCS. Springer-Verlag, 1994."},{"key":"14_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the First International Conference Formal Methods in Computer-Aided Design\u2019 96","author":"D. Cyrluk","year":"1996","unstructured":"D. Cyrluk. Inverting the Abstraction Mapping: A Methodology for Hardware Verification. In M. Srivas and A. Camilleri, editors, Proc. of the First International Conference Formal Methods in Computer-Aided Design\u2019 96, volume 1166 of LNCS, Berlin, 1996. Springer-Verlag."},{"key":"14_CR5","unstructured":"M. P. Fourman. Proof and design: Machine-assisted formal proof as a basis for foundation of computer science. LFCS report ECS-LFCS-95-319, Laboratory for Foundation of Computer Science, The University of Edinburgh, Edinburgh, 1995."},{"key":"14_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of International Workshop on Hardware Specification, and Synthesis: Mathematical Aspects","author":"K. Hanna","year":"1990","unstructured":"K. Hanna, N. Daeche, and M. Longley. Veritas+: A Specification Language Based on Type Theory. In M. E. Lesser and G. M. Brown, editors, Proc. of International Workshop on Hardware Specification, and Synthesis: Mathematical Aspects, volume 408 of LNCS, New York, 1990. Springer-Verlag."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"C. Hoare. Proof of Correctness of Data Representation. Acta Informatica, 1, 1972.","DOI":"10.1007\/BF00289507"},{"key":"14_CR8","unstructured":"H. Jifeng and C. Hoare. Data Refinement in a Categorical Setting. Technical Monograph PRG-90, Oxford University Computing Laboratory, Programming Research Group, Oxford, 1990."},{"key":"14_CR9","unstructured":"G. Jones and M. Sheeran. Circuit Design in Ruby. In J. Staunstrup, editor, Formal Methods for VLSI Design, IFIPWG 10.5 Lecture Notes, chapter 1. North-Holland, Amsterdam, 1990."},{"key":"14_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of Third International Symposium on Theoretical Aspects of Computer Software\u2019 97","author":"Y. Kinoshita","year":"1997","unstructured":"Y. Kinoshita, P. O\u2019Hearn, A. Power, M. Takeyama, and R. Tennent. An Axiomatic Approach to Binary Logical Relation with Applications to Data Refinement. In M. Abadi and T. Ito, editors, Proc. of Third International Symposium on Theoretical Aspects of Computer Software\u2019 97, volume 1281 of LNCS, Berlin, 1997. Springer-Verlag."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Y. Kinoshita, A. Power, and M. Takeyama. Sketches. Electronic Notes in The-oretical Computer Science, 6, 1997. URL: http:\/\/www.elsevier.nl\/locate\/ entcs\/volume6.html.","DOI":"10.1016\/S1571-0661(05)80158-6"},{"key":"14_CR12","unstructured":"J. Lambek and P. Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge studies in advanced mathematics. Cambridge University Press, 1986."},{"key":"14_CR13","volume-title":"Categories for the Working Mathematician","author":"S. Mac Lane","year":"1998","unstructured":"S. Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, New York, 2nd edition, 1998.","edition":"2nd edition"},{"key":"14_CR14","unstructured":"J. Mitchell. Foundations for Programming Language. Foundations of Computing Series. MIT Press, 1996."},{"key":"14_CR15","unstructured":"N. Sabadini, R. Walters, and H. Weld. On categories of asynchronous circuits. http:\/\/cat.maths.usyd.edu.au\/~bob\/papers\/asyncirci.ps, 1994."},{"key":"14_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of International Workshop on Hardware Specification, and Synthesis: Mathematical Aspects","author":"M. Sheeran","year":"1990","unstructured":"M. Sheeran. Categories for the Working Hardware Designer. In M. E. Lesser and G. M. Brown, editors, Proc. of International Workshop on Hardware Specification, and Synthesis: Mathematical Aspects, volume 408 of LNCS, New York, 1990. Springer-Verlag."},{"key":"14_CR17","unstructured":"P. Taylor. Commutative Diagrams in TEX(version 4). Department of Computer Science, Queen Mary and Westfield College, London, 1997."},{"key":"14_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the Second International Conference Formal Methods in Computer-Aided Design\u2019 98","author":"M. N. Velev","year":"1998","unstructured":"M. N. Velev and R. E. Bryant. Bit-Level Abstractiion in the Verification of Pipelined Microprocessors by Correspondence Checking. In G. Gopalakrishnan and P. Windley, editors, Proc. of the Second International Conference Formal Methods in Computer-Aided Design\u2019 98, volume 1522 of LNCS, Berlin, 1998. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN\u201999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46674-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T08:56:36Z","timestamp":1557046596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46674-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668565","9783540466741"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-46674-6_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}