{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:06:22Z","timestamp":1737435982797,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540741299"},{"type":"electronic","value":"9783540741305"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74130-5_6","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T15:32:56Z","timestamp":1187019176000},"page":"91-107","source":"Crossref","is-referenced-by-count":1,"title":["Low-Level Programming in Hume: An Exploration of the HW-Hume Level"],"prefix":"10.1007","author":[{"given":"Kevin","family":"Hammond","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gudmund","family":"Grov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Greg","family":"Michaelson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Ireland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Electronic Design Interchange Format Version 2.0.0,Technical ANSI\/EIA-548-1988 (1988)"},{"key":"6_CR2","unstructured":"Confluence (2006), http:\/\/www.confluent.org\/wiki\/doku.php?id=confluence"},{"key":"6_CR3","unstructured":"Hdcaml (2006), http:\/\/www.confluent.org\/wiki\/doku.php"},{"key":"6_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters\u00a021, 181\u2013185 (1985)","journal-title":"Information Processing Letters"},{"key":"6_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2714-2","volume-title":"Verification of Sequential and Concurrent Programs","author":"K.R. Apt","year":"1997","unstructured":"Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 2nd edn. Springer, Heidelberg (1997)","edition":"2"},{"issue":"1","key":"6_CR6","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1145\/291251.289440","volume":"34","author":"P. Bjesse","year":"1999","unstructured":"Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: Hardware design in Haskell. ACM SIGPLAN Notices\u00a034(1), 174\u2013184 (January 1999)","journal-title":"ACM SIGPLAN Notices"},{"key":"6_CR7","first-page":"235","volume-title":"IFL 2006","author":"A. Bonenfant","year":"2007","unstructured":"Bonenfant, A., Ferdinand, C., Hammond, K., Heckmann, R.: Worst-Case Execution Times for a Purely Functional Language. In: Horv\u00e1th, Z, Zs\u00f3k, V., Butterfield, A. (eds.) IFL 2006, vol.\u00a04449, pp. 235\u2013252. Springer, Heidelberg (2007)"},{"issue":"9","key":"6_CR8","doi-asserted-by":"publisher","first-page":"1293","DOI":"10.1109\/5.97299","volume":"79","author":"F. Boussinot","year":"1991","unstructured":"Boussinot, F., de Simone, R.: The Esterel Language. Proceedings of the IEEE\u00a079(9), 1293\u20131304 (1991)","journal-title":"Proceedings of the IEEE"},{"issue":"3","key":"6_CR9","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/s10009-004-0181-6","volume":"7","author":"A. Butterfield","year":"2005","unstructured":"Butterfield, A., Woodcock, J.: prialt in Handel-C: an operational semantics. Int. J. Softw. Tools Technol. Transf.\u00a07(3), 248\u2013267 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Place, J.: Lustre: a Declarative Language for Programming Synchronous Systems. In: Proc. POPL 1987 Symposium on Principles of Programming Languages, M\u00fcnchen, Germany, pp. 178\u2013188 (January 1987)","DOI":"10.1145\/41625.41641"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Claessen, K., Pace, G.: An Embedded Language Framework for Hardware Compilation. In: Proc. Conf. on Designing Correct Circuits (DCC 2002) (2002)","DOI":"10.1145\/636517.636526"},{"key":"6_CR12","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"6_CR13","first-page":"180","volume-title":"Proc. POPL 2006: ACM Symposium on Principles of Programming Languages","author":"A. Cohen","year":"2006","unstructured":"Cohen, A., Duranton, M., Eisenbeis, C., Pagetti, C., Plateau, F., Pouzet, M.: N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In: Proc. POPL 2006: ACM Symposium on Principles of Programming Languages, pp. 180\u2013193. ACM Press, New York (2006)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.-L., Pagano, B., Pouzet, M.: A Conservative Extension of Synchronous Data-flow with State Machines. In: Proc. ACM International Conference on Embedded Software (EMSOFT 2005), Jersey City, New Jersey, USA (September 2005)","DOI":"10.1145\/1086228.1086261"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"6_CR16","unstructured":"Foster, J.N.: Model Checking for a Functional Hardware Description Language, BSc Dissertation, Cambridge University. PhD thesis (2002)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/3-540-18317-5_15","volume-title":"Functional Programming Languages and Computer Architecture","author":"T. Gautier","year":"1987","unstructured":"Gautier, T., Le Guernic, P., Besnard, L.: SIGNAL: A Declarative Language For Synchronous Programming of Real-Time Systems. In: Kahn, G. (ed.) Functional Programming Languages and Computer Architecture. LNCS, vol.\u00a0274, pp. 257\u2013277. Springer, Heidelberg (1987)"},{"key":"6_CR18","unstructured":"Grov, G., Ireland, A., Michaelson, G.J., Hammond, K.: Verifying Temporal Properties in HW-Hume. Technical report, Heriot-Watt University, School of Mathematical and Computer Sciences (February 2006)"},{"issue":"2","key":"6_CR19","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1017\/S0956796805005757","volume":"16","author":"J. Grundy","year":"2006","unstructured":"Grundy, J., Melham, T., O\u2019Leary, J.: A Reflective Functional Language for Hardware Design and Theorem Proving. J. Funct. Program\u00a016(2), 157\u2013196 (2006)","journal-title":"J. Funct. Program"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Hammond, K.: Exploiting Purely Functional Programming to Obtain Bounded Resource Behaviour: the Hume Approach. In: Central European Summer School on Functional Programming, July 2005. Spinger-Verlag LNCS (to appear)","DOI":"10.1007\/11894100_4"},{"key":"6_CR21","unstructured":"Hammond, K., Michaelson, G.: Bounded Space Programming using Finite State Machines and Recursive Functions: the Hume Approach. Submitted to ACM Transactions on Software Engineering and Methodology (TOSEM 2006) (in preparation)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-540-39815-8_3","volume-title":"Generative Programming and Component Engineering","author":"K. Hammond","year":"2003","unstructured":"Hammond, K., Michaelson, G.J.: Hume: a Domain-Specific Language for Real-Time Embedded Systems. In: Pfenning, F., Smaragdakis, Y. (eds.) GPCE 2003. LNCS, vol.\u00a02830, pp. 37\u201356. Springer, Heidelberg (2003)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44854-3_1","volume-title":"Implementation of Functional Languages","author":"K. Hammond","year":"2003","unstructured":"Hammond, K., Michaelson, G.J.: Predictable Space Behaviour in FSM-Hume. In: Pe\u00f1a, R., Arts, T. (eds.) IFL 2002. LNCS, vol.\u00a02670, Springer, Heidelberg (2003)"},{"issue":"4","key":"6_CR24","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model Checking JAVA Programs using JAVA PathFinder. Int. Journal on Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1007\/3-540-45706-2_85","volume-title":"Euro-Par 2002. Parallel Processing","author":"J. Hawkins","year":"2002","unstructured":"Hawkins, J., Abdallah, A.E.: Behavioural Synthesis of a Parallel Hardware JPEG Decoder from a Functional Specification. In: Monien, B., Feldmann, R.L. (eds.) Euro-Par 2002. LNCS, vol.\u00a02400, pp. 615\u2013619. Springer, Heidelberg (2002)"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Launchbury, J., Matthews, J., Cook, B.: Microprocessor Specification in Hawk. In: Proc. International Conference on Computer Languages, pp. 90\u2013101 (1998)","DOI":"10.1109\/ICCL.1998.674160"},{"key":"6_CR27","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 (1990)"},{"issue":"3","key":"6_CR28","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The Temporal Logic of Actions. ACM TOPLAS\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM TOPLAS"},{"key":"6_CR29","volume-title":"Specifying Systems \u2014 The TLA+ Language and Tools for Hardware and Software Engineers","author":"L. Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems \u2014 The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading, Massachusetts (2002)"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11560548_14","volume-title":"Correct Hardware Design and Verification Methods","author":"L. Lamport","year":"2005","unstructured":"Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 162\u2013175. Springer, Heidelberg (2005)"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Mycroft, A., Sharp, R.: A Statically Allocated Parallel Functional Language. Automata, Languages and Programming, pp. 37\u201348 (2000)","DOI":"10.1007\/3-540-45022-X_5"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45319-9_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Mycroft","year":"2001","unstructured":"Mycroft, A., Sharp, R.: Hardware\/Software Co-Design Using Functional Languages. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 236\u2013251. Springer, Heidelberg (2001)"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","first-page":"184","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"C.B. Earle","year":"2002","unstructured":"Earle, C.B., Arts, T., Derrick, J.: Verifying Erlang Code: a Resource Locker Case-Study. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 184\u2013203. Springer, Heidelberg (2002)"},{"key":"6_CR34","unstructured":"Vasconcelos, P.B.: Cost Inference and Analysis for Recursive Functional Programs. PhD thesis, University of St Andrews (in preparation)"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-540-27861-0_6","volume-title":"Implementation of Functional Languages","author":"P.B. Vasconcelos","year":"2004","unstructured":"Vasconcelos, P.B., Hammond, K.: Inferring Costs for Recursive, Polymorphic and Higher-Order Functional Programs. In: Trinder, P., Michaelson, G.J., Pe\u00f1a, R. (eds.) IFL 2003. LNCS, vol.\u00a03145, pp. 86\u2013101. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Functional Languages"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74130-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T09:20:50Z","timestamp":1737364850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74130-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540741299","9783540741305"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74130-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}