{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:20:28Z","timestamp":1725488428138},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425250"},{"type":"electronic","value":"9783540447559"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_15","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:03:32Z","timestamp":1186740212000},"page":"201-216","source":"Crossref","is-referenced-by-count":2,"title":["Abstraction and Refinement in Higher Order Logic"],"prefix":"10.1007","author":[{"given":"Matt","family":"Fairtlough","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaochun","family":"Cheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"15_CR1","volume-title":"Design Methodologies for VLSI and Computer Architecture","author":"H. Eveking","year":"1989","unstructured":"H. Eveking. Behavioural consistency between register-transfer-and switch-level descriptions. In D. A. Edwards, editor, Design Methodologies for VLSI and Computer Architecture. Elsevier Science, B. V., 1989."},{"key":"15_CR2","unstructured":"M. Fairtlough, M. Mendler, and M. Walton. First-order Lax Logic as a Framework for CLP. Technical Report MIPS-9714, Passau University, Department of Mathematics and Computer Science, 1997."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"M. Fairtlough and M. V. Mendler. Propositional Lax Logic. Information and Computation, 137(1):1\u201333, August 1997.","DOI":"10.1006\/inco.1997.2627"},{"key":"15_CR4","unstructured":"M. Fairtlough and M. Walton. Quantified Lax Logic. Technical Report CS-97-11, Sheffield University, Department of Computer Science, 1997."},{"key":"15_CR5","unstructured":"M.P. Fourman. Proof and design. Technical Report ECS-LFCS-95-319, Edinburgh University, Department of Computer Science, 1995."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"M.P. Fourman and R.A. Hexsel. Formal synthesis. In G. Birtwistle, editor, Proceedings of the IV Higher Order Workshop, Banff, 1990, 1991.","DOI":"10.1007\/978-1-4471-3182-3_14"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0004-3702(92)90021-O","volume":"57","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia and T. Walsh. A theory of abstraction. Artificial Intelligence, 57:323\u2013389, 1992.","journal-title":"Artificial Intelligence"},{"key":"15_CR8","unstructured":"F.K. Hanna and N. Daeche. Specification and verification using higher order logic: A case study. In G. M. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI design, Proc. of the 1985 Edinburgh conf. on VLSI, pages 179\u2013213. North-Holland, 1986."},{"key":"15_CR9","first-page":"668","volume-title":"IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design","author":"J. Herbert","year":"1989","unstructured":"J. Herbert. Formal reasoning about timing and function of basic memory devices. In Dr. Luc Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 2, pages 668\u2013687. Elsevier Science Publishers, B.V., 1989."},{"key":"15_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/BFb0037108","volume-title":"Typed Lambda Calculi and Applications, TLCA\u201993","author":"B. Jacobs","year":"1993","unstructured":"B. Jacobs and T. Melham. Translating dependent type theory into higher order logic. In Typed Lambda Calculi and Applications, TLCA\u201993, pages 209\u2013229. Springer LNCS 664, 1993."},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"J.H. McKinna. Deliverables: A Categorical Approach to Program Development in Type Theory. PhD thesis, Edinburgh University, Department of Computer Science, 1992.","DOI":"10.1007\/3-540-57182-5_3"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"T.F. Melham. Higher Order Logic and Hardware Verification. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511569845"},{"key":"15_CR13","unstructured":"M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS-93-255, 1993."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"M. Mendler. Timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proc. 5th Int. Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 261\u2013277. Springer, 1996.","DOI":"10.1007\/3-540-61208-4_17"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"M. Mendler and M. Fairtlough. Ternary simulation: A refinement of binary functions or an abstraction of real-time behaviour? In M. Sheeran and S. Singh, editors, Proc. 3rd Workshop on Designing Correct Circuits (DCC\u201996). Springer Electronic Workshops in Computing, 1996.","DOI":"10.14236\/ewic\/DCC1996.8"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D.A. Plaisted","year":"1981","unstructured":"D.A. Plaisted. Theorem proving with abstraction. Artificial Intelligence, 16:47\u2013108, 1981.","journal-title":"Artificial Intelligence"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"A.S. Troelstra. Realizability. In S. Buss, editor, Handbook of Proof Theory. Elsevier Science B.V., 1998.","DOI":"10.1016\/S0049-237X(98)80021-9"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T19:32:04Z","timestamp":1587843124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}