{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:06:27Z","timestamp":1759147587259,"version":"3.43.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1997,10,1]],"date-time":"1997-10-01T00:00:00Z","timestamp":875664000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,10,1]],"date-time":"1997-10-01T00:00:00Z","timestamp":875664000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1997,10]]},"DOI":"10.1023\/a:1008603713967","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"239-264","source":"Crossref","is-referenced-by-count":12,"title":["The T-Ruby Design System"],"prefix":"10.1007","volume":"11","author":[{"given":"Robin","family":"Sharp","sequence":"first","affiliation":[]},{"given":"Ole","family":"Rasmussen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"142122_CR1","unstructured":"H. Busch, \u201cTransformational design in a theorem prover,\u201d in V. Stavridou, T.F. Melham, and R.T. Boute (Eds.), Theorem Provers in Circuit Design, IFIP WG10.2, North-Holland, 1992, pp. 175-196."},{"key":"142122_CR2","first-page":"207","volume-title":"Computer Hardware Description Languages, CHDL'93","author":"A. Dent","year":"1993","unstructured":"A. Dent and K. Hanna, \u201cReasoning about array structures using a dependently typed logic,\u201d in D. Agnew, L. Claesen, and R. Camposano (Eds.), Computer Hardware Description Languages, CHDL'93, IFIP WG10.2, North-Holland, 1993, pp. 207-224."},{"key":"142122_CR3","unstructured":"F.K. Hanna, M. Langley, and N. Daeche, \u201dFormal synthesis of digital systems,\u201d in L.J.M. Claesen (Ed.), VLSI Design Methods, North-Holland, 1990, Vol. 1, pp. 153-169."},{"key":"142122_CR4","volume-title":"Ph.D. Thesis","author":"G. Hutton","year":"1993","unstructured":"G. Hutton, Between Functions and Relations in Calculating Programs, Ph.D. Thesis, Department of Computer Science, University of Glasgow, June 1993."},{"key":"142122_CR5","first-page":"13","volume-title":"Formal Methods for VLSI Design","author":"G. Jones","year":"1990","unstructured":"G. Jones and M. Sheeran, \u201cCircuit design in Ruby,\u201d in J\u00f8rgen Staunstrup (Ed.), Formal Methods for VLSI Design, Elsevier Science Publishers, B.V., 1990, pp. 13-70."},{"key":"142122_CR6","unstructured":"G. Jones and M. Sheeran, \u201cRelations and refinement in circuit design,\u201d in C.C. Morgan and J.C.P. Woodcock (Eds.), Proceedings of the 3rd BCS FACSWorkshop on Refinement, Workshops in Computing, BCS, Springer-Verlag, London, Jan. 1991, pp. 133-152."},{"key":"142122_CR7","volume-title":"Licentiate Thesis 378","author":"M. Larsson","year":"1993","unstructured":"M. Larsson, \u201cA Transformational Approach to Formal Digital System Design,\u201d Licentiate Thesis 378, Dept. of Computer And Information Science, Link\u00f6ping University, May 1993."},{"key":"142122_CR8","doi-asserted-by":"crossref","unstructured":"W. Luk, \u201cA declarative approach to incremental custom computing,\u201d in Proceedings of IEEE Symposium on FCCM, IEEE Computer Society Press, 1995, pp. 164-172.","DOI":"10.1109\/FPGA.1995.477422"},{"key":"142122_CR9","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f, \u201cConstructive mathematics and computer programming,\u201d in C.A.R. Hoare and J.C. Shepherdson (Eds.), Mathematical Logic and Programming Languages, Prentice-Hall, London, 1985, pp. 167-184. Also published in Proc. 6th. International Congress for Logic, Methodology and Philosophy of Science, North-Holland, 1982, pp. 153-175.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"142122_CR10","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, Isabelle: A Generic Theorem Prover, Vol. 828 of Lecture Notes in Computer Science, Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"142122_CR11","first-page":"225","volume-title":"Computer Hardware Description Languages, CHDL'93","author":"L. Pierre","year":"1993","unstructured":"L. Pierre, \u201cVHDL description and formal verification of systolic multipliers,\u201d in D. Agnew, L. Claesen, and R. Camposano (Eds.), Computer Hardware Description Languages, CHDL'93, IFIP WG10.2, North-Holland, 1993, pp. 225-242."},{"key":"142122_CR12","doi-asserted-by":"crossref","unstructured":"O. Rasmussen, \u201cAn embedding of Ruby in Isabelle,\u201d in M.A. McRobbie and J.K. Slaney (Eds.), Automated Deduction: CADE 13, Lecture Notes in Artificial Intelligence, Springer, July 1996, pp. 186-200.","DOI":"10.1007\/3-540-61511-3_80"},{"key":"142122_CR13","doi-asserted-by":"crossref","unstructured":"O. Rasmussen, \u201cEnsuring correctness of Ruby transformations,\u201d in C.J. van Rijsbergen (Ed.), Designing Correct Circuits '96, Electronic Workshops in Computing, Springer, 1996.","DOI":"10.14236\/ewic\/DCC1996.11"},{"key":"142122_CR14","first-page":"179","volume-title":"Formal Methods for VLSI Design","author":"L. Rossen","year":"1990","unstructured":"L. Rossen, \u201cFormal Ruby,\u201d in J\u00f8rgen Staunstrup (Ed.), Formal Methods for VLSI Design, Elsevier Science Publishers, B.V., 1990, pp. 179-190."},{"key":"142122_CR15","doi-asserted-by":"crossref","unstructured":"L. Rossen, 'Proving (facts about) Ruby,\u201d in G. Birtwhistle (Ed.), IV Higher Order Workshop, Banff, Workshops in Computing, Springer-Verlag, 1990, pp. 265-283.","DOI":"10.1007\/978-1-4471-3182-3_15"},{"key":"142122_CR16","doi-asserted-by":"crossref","unstructured":"L. Rossen, \u201cRuby algebra,\u201d in G. Jones and M. Sheeran (Ed.), Designing Correct Circuits, Oxford 1990, Workshops in Computing, Springer-Verlag, 1990, pp. 297-312.","DOI":"10.1007\/978-1-4471-3544-9_16"},{"key":"142122_CR17","volume-title":"Technical Report ID-TR: 1994-153","author":"O. Sandum","year":"1994","unstructured":"O. Sandum, \u201cMultiple clocks and Ruby,\u201d Technical Report ID-TR: 1994-153, Dept. of Computer Science, Technical University of Denmark, Aug. 1994."},{"key":"142122_CR18","doi-asserted-by":"crossref","unstructured":"R. Schl\u00f6r, \u201cA prover for VHDL-based hardware design,\u201d in S.D. Johnson (Ed.), Computer Hardware Description Languages, CHDL'95, IFIP WG10.5, IEEE, 1995, pp. 643-650.","DOI":"10.1109\/ASPDAC.1995.486382"},{"key":"142122_CR19","volume-title":"Technical Report ID-TR: 1993-119","author":"R. Sharp","year":"1993","unstructured":"R. Sharp, \u201cThe Ruby framework,\u201d Technical Report ID-TR: 1993-119, Dept. of Computer Science, Technical University of Denmark, June 1993."},{"key":"142122_CR20","volume-title":"Technical Report ID-TR: 1994-154","author":"R. Sharp","year":"1994","unstructured":"R. Sharp, \u201cT-Ruby: A tool for handling Ruby expressions,\u201d Technical Report ID-TR: 1994-154, Dept. of Computer Science, Technical University of Denmark, Dec. 1994. (On-line version at URL uhttp:\/\/www.it.dtu.dk\/~ruby\/manual\/manual.html)"},{"key":"142122_CR21","doi-asserted-by":"crossref","unstructured":"R. Sharp and O. Rasmussen, \u201cTransformational rewriting with Ruby,\u201d in L. Claesen (Ed.), Computer Hardware Description Languages, CHDL'93, IFIP WG10.2, Elsevier Science Publishers, B.V., 1993, pp. 243-260.","DOI":"10.1016\/B978-0-444-81641-2.50024-1"},{"key":"142122_CR22","unstructured":"Synopsys Inc., VHDL Compiler Reference Manual, 3.1 edition, 1994."},{"key":"142122_CR23","first-page":"359","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"J.P. Van Tassel","year":"1992","unstructured":"J.P. Van Tassel, \u201cA formalisation of the VHDL simulation cycle,\u201d in L.J.M. Claesen and M.J.C. Gordon (Eds.), Higher Order Logic Theorem Proving and its Applications, IFIP WG10.2, North-Holland, 1992, pp. 359-374."},{"key":"142122_CR24","doi-asserted-by":"crossref","unstructured":"D. Weise, \u201cConstraints, abstraction and verification,\u201d in M. Leeser and G. Brown (Eds.), Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects, Vol. 408 of Lecture Notes in Computer Science, Springer-Verlag, 1989, pp. 25-39.","DOI":"10.1007\/0-387-97226-9_22"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008603713967.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008603713967\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008603713967.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:50:11Z","timestamp":1754369411000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008603713967"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,10]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,10]]}},"alternative-id":["142122"],"URL":"https:\/\/doi.org\/10.1023\/a:1008603713967","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1997,10]]}}}