{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,20]],"date-time":"2023-08-20T12:59:29Z","timestamp":1692536369156},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2006,10,19]],"date-time":"2006-10-19T00:00:00Z","timestamp":1161216000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,17]]},"DOI":"10.1007\/s10817-006-9039-9","type":"journal-article","created":{"date-parts":[[2006,10,18]],"date-time":"2006-10-18T08:35:02Z","timestamp":1161160502000},"page":"117-152","source":"Crossref","is-referenced-by-count":6,"title":["Verification of FPGA Layout Generators in Higher-Order Logic"],"prefix":"10.1007","volume":"37","author":[{"given":"Oliver","family":"Pell","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,10,19]]},"reference":[{"key":"9039_CR1","unstructured":"IEEE: IEEE standard VHDL language reference manual, IEEE Std. pp. 1076\u20131987. New York (1998)"},{"key":"9039_CR2","unstructured":"DS031: Virtex-II platform FPGAs: complete data sheet, Xilinx, Inc., San Jose, California (2005)"},{"key":"9039_CR3","first-page":"400","volume-title":"HUG\u201993, vol. 780 of LNCS","author":"M. Aagaard","year":"1993","unstructured":"Aagaard, M., Leeser, M., Windley, P.: Towards a super duper hardware tactic. In: HUG\u201993, vol. 780 of LNCS, pp. 400\u2013412. Springer, Berlin Heidelberg New York (1993)"},{"issue":"7","key":"9039_CR4","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0895-7177(93)90068-A","volume":"17","author":"A. Aggoun","year":"1993","unstructured":"Aggoun, A., Beldiceanu, N.: Extending CHIP in order to solve complex scheduling and placement problems. J. Math. Comput. Model. 17(7), 57\u201373 (1993)","journal-title":"J. Math. Comput. Model."},{"key":"9039_CR5","doi-asserted-by":"crossref","unstructured":"Andraka, R.: A survey of CORDIC algorithms for FPGA based computers. In: Proceedings FPGA \u201998: 6th ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, pp. 191\u2013200. New York (1998)","DOI":"10.1145\/275107.275139"},{"key":"9039_CR6","first-page":"377","volume-title":"Proceedings Constraint Programming 2001, vol. 2239 of LNCS","author":"N. Beldiceanu","year":"2001","unstructured":"Beldiceanu, N., Carlsson, M.: Sweep as a generic pruning technique applied to the non-overlapping rectangles constraint. In: Walsh, T. (ed.) Proceedings Constraint Programming 2001, vol. 2239 of LNCS, pp. 377\u2013391. Springer, Berlin Heidelberg New York (2001)"},{"key":"9039_CR7","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: hardware design in Haskell. In: Proceedings ICFP \u201998: 3rd ACM SIGPLAN International Conference on Functional Programming, pp. 174\u2013184. New York (1998)","DOI":"10.1145\/289423.289440"},{"key":"9039_CR8","first-page":"129","volume-title":"IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience","author":"R. Boulton","year":"1992","unstructured":"Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in HOL. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds.) IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pp. 129\u2013156. North-Holland, Amsterdam, The Netherlands (1992)"},{"key":"9039_CR9","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic, New York (1979)"},{"key":"9039_CR10","first-page":"203","volume-title":"Proceedings TPCD\u201994: 2nd International Conference on Theorem Provers in Circuit Design","author":"D. Cyrluk","year":"1994","unstructured":"Cyrluk, D., Rajan, S., Shankar, N., Srivas, M.K.: Effective theorem proving for hardware verification. In: Proceedings TPCD\u201994: 2nd International Conference on Theorem Provers in Circuit Design, pp. 203\u2013222. Bad Herrenalb, Germany (1994)"},{"key":"9039_CR11","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings POPL \u201982: 9th ACM Symposium on Principles of Programming Languages, pp. 207\u2013212. New York (1982)","DOI":"10.1145\/582153.582176"},{"issue":"3\u20134","key":"9039_CR12","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/S1383-7621(00)00052-7","volume":"47","author":"S. Guo","year":"2001","unstructured":"Guo, S., Luk, W.: An integrated system for developing regular array designs. J. Systems Archit. 47(3\u20134), 315\u2013337 (2001)","journal-title":"J. Systems Archit."},{"key":"9039_CR13","first-page":"29","volume":"146","author":"R. Hindley","year":"1969","unstructured":"Hindley, R.: The principal type scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29\u201360 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"9039_CR14","first-page":"13","volume-title":"Formal Methods for VLSI Design","author":"G. Jones","year":"1990","unstructured":"Jones, G., Sheeran, M.: Circuit design in Ruby. In: Staunstrup, J. (ed.) Formal Methods for VLSI Design, pp. 13\u201370. North-Holland, Amsterdam, The Netherlands (1990)"},{"issue":"4","key":"9039_CR15","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Softw. Eng. 23(4), 203\u2013213 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9039_CR16","first-page":"9","volume-title":"Proceedings FPL\u201998: Field-Programmable Logic and Applications, vol. 1482 of LNCS","author":"W. Luk","year":"1998","unstructured":"Luk, W., McKeever, S.: Pebble: a language for parameterised and reconfigurable hardware design. In: Hartenstein, R.W., Keevallik, A. (eds.) Proceedings FPL\u201998: Field-Programmable Logic and Applications, vol. 1482 of LNCS, pp. 9\u201318. Springer, Berlin Heidelberg New York (1998)"},{"key":"9039_CR17","first-page":"288","volume-title":"Proceedings CAV\u201999: Computer Aided Verification, vol. 1633 of LNCS","author":"J. Matthews","year":"1999","unstructured":"Matthews, J., Launchbury, J.: Elementary microarchitecture algebra. In: Proceedings CAV\u201999: Computer Aided Verification, vol. 1633 of LNCS, pp. 288\u2013300. Springer, Berlin Heidelberg New York (1999)"},{"key":"9039_CR18","first-page":"342","volume-title":"Proceedings FMCAD 2002: 4th International Conference on Formal Methods in Computer-Aided Design, vol. 2517 of LNCS","author":"S. McKeever","year":"2002","unstructured":"McKeever, S., Luk, W., Derbyshire, A.: Compiling hardware descriptions with relative placement information for parameterised libraries. In: Aagaard, M., O\u2019Leary, J. (eds.) Proceedings FMCAD 2002: 4th International Conference on Formal Methods in Computer-Aided Design, vol. 2517 of LNCS, pp. 342\u2013359. Springer, Berlin Heidelberg New York (2002)"},{"key":"9039_CR19","doi-asserted-by":"crossref","unstructured":"McKeever, S., Luk, W., Derbyshire, A.: Towards verifying parametrised hardware libraries with relative placement information. In: Proceedings HICSS \u201903: 36th Hawaii International Conference on System Sciences, p.\u00a010. Washington, District of Columbia (2003)","DOI":"10.1109\/HICSS.2003.1174812"},{"key":"9039_CR20","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569845","volume-title":"Higher Order Logic and Hardware Verification, Cambridge Tracts in Theoretical Computer Science","author":"T. Melham","year":"1993","unstructured":"Melham, T.: Higher Order Logic and Hardware Verification, Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK (1993)"},{"key":"9039_CR21","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"9039_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283 of LNCS","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283 of LNCS. Springer, Berlin Heidelberg New York (2002)"},{"key":"9039_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover, vol. 828 of LNCS","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover, vol. 828 of LNCS. Springer, Berlin Heidelberg New York (1994)"},{"key":"9039_CR24","volume-title":"Proceedings RECONFIG\u201905: International Conference on Reconfigurable Computing and FPGAs","author":"O. Pell","year":"2005","unstructured":"Pell, O., Luk, W.: Quartz: a framework for correct and efficient reconfigurable design. In: Proceedings RECONFIG\u201905: International Conference on Reconfigurable Computing and FPGAs. IEEE Computer Society Press, Los Alamitos, California (2005a)."},{"key":"9039_CR25","first-page":"380","volume-title":"Proceedings CHARME\u201905: 13th Conference on Correct Hardware Design and Verification Methods, vol. 3725 of LNCS","author":"O. Pell","year":"2005","unstructured":"Pell, O., Luk, W.: Resolving quartz overloading. In: Borrione, D., Paul, W. (eds.) Proceedings CHARME\u201905: 13th Conference on Correct Hardware Design and Verification Methods, vol. 3725 of LNCS, pp. 380\u2013383. Springer, Berlin Heidelberg New York (2005b)"},{"key":"9039_CR26","first-page":"186","volume-title":"Proceedings CADE: 13th International Conference on Automated Deduction, vol. 1104 of LNCS","author":"O. Rasmussen","year":"1996","unstructured":"Rasmussen, O.: An embedding of Ruby in Isabelle. In: Slaney, J.K. (ed.) Proceedings CADE: 13th International Conference on Automated Deduction, vol. 1104 of LNCS, pp. 186\u2013200. Springer, Berlin Heidelberg New York (1996)"},{"key":"9039_CR27","doi-asserted-by":"crossref","unstructured":"Singh, S.: Death of the RLOC? In: Proceedings FCCM\u201900: 8th IEEE Symposium on Field-Programmable Custom Computing Machines, pp. 145\u2013152. Washington, District of Columbia (2000)","DOI":"10.1109\/FPGA.2000.903401"},{"key":"9039_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2464-6","volume-title":"The Verilog Hardware Description Language","author":"D.E. Thomes","year":"1996","unstructured":"Thomes, D.E., Moorby, P.: The Verilog Hardware Description Language. Kluwer, Norwell, Massachusetts 3rd edn. (1996)","edition":"3"},{"key":"9039_CR29","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad hoc polymorphism less ad hoc. In: Proceedings POPL \u201989: 16th ACM Symposium on Principles of Programming Languages, pp. 60\u201376. New York (1989)","DOI":"10.1145\/75277.75283"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9039-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9039-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9039-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:46Z","timestamp":1559265706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9039-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,19]]},"references-count":29,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,1,17]]}},"alternative-id":["9039"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9039-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10,19]]}}}