Skip to main content
SpringerLink
Log in

Low-Level Programming in Hume: An Exploration of the HW-Hume Level

  • Conference paper
Book cover Implementation and Application of Functional Languages (IFL 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4449))

Included in the following conference series:

Abstract

This paper describes the HW-Hume level of the novel Hume language. HW-Hume is the simplest subset of Hume that we have identified. It provides strong formal properties but posseses limited abstraction capabilities. In this paper, we introduce HW-Hume, show some simple example programs, describe an efficient software implementation, and demonstrate how important properties can be exposed as part of an integrated formally-based verification approach.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Electronic Design Interchange Format Version 2.0.0,Technical ANSI/EIA-548-1988 (1988)

    Google Scholar 

  2. Confluence (2006), http://www.confluent.org/wiki/doku.php?id=confluence

  3. Hdcaml (2006), http://www.confluent.org/wiki/doku.php

  4. Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  5. Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 2nd edn. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  6. Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: Hardware design in Haskell. ACM SIGPLAN Notices 34(1), 174–184 (January 1999)

    Article  Google Scholar 

  7. Bonenfant, A., Ferdinand, C., Hammond, K., Heckmann, R.: Worst-Case Execution Times for a Purely Functional Language. In: Horváth, Z, Zsók, V., Butterfield, A. (eds.) IFL 2006, vol. 4449, pp. 235–252. Springer, Heidelberg (2007)

    Google Scholar 

  8. Boussinot, F., de Simone, R.: The Esterel Language. Proceedings of the IEEE 79(9), 1293–1304 (1991)

    Article  Google Scholar 

  9. Butterfield, A., Woodcock, J.: prialt in Handel-C: an operational semantics. Int. J. Softw. Tools Technol. Transf. 7(3), 248–267 (2005)

    Article  Google Scholar 

  10. 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ünchen, Germany, pp. 178–188 (January 1987)

    Google Scholar 

  11. Claessen, K., Pace, G.: An Embedded Language Framework for Hardware Compilation. In: Proc. Conf. on Designing Correct Circuits (DCC 2002) (2002)

    Google Scholar 

  12. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  13. 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–193. ACM Press, New York (2006)

    Google Scholar 

  14. Colaço, 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)

    Google Scholar 

  15. Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Foster, J.N.: Model Checking for a Functional Hardware Description Language, BSc Dissertation, Cambridge University. PhD thesis (2002)

    Google Scholar 

  17. 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. 274, pp. 257–277. Springer, Heidelberg (1987)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. Grundy, J., Melham, T., O’Leary, J.: A Reflective Functional Language for Hardware Design and Theorem Proving. J. Funct. Program 16(2), 157–196 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  20. 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)

    Google Scholar 

  21. 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)

    Google Scholar 

  22. 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. 2830, pp. 37–56. Springer, Heidelberg (2003)

    Google Scholar 

  23. Hammond, K., Michaelson, G.J.: Predictable Space Behaviour in FSM-Hume. In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  24. Havelund, K., Pressburger, T.: Model Checking JAVA Programs using JAVA PathFinder. Int. Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)

    Article  MATH  Google Scholar 

  25. 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. 2400, pp. 615–619. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Launchbury, J., Matthews, J., Cook, B.: Microprocessor Specification in Hawk. In: Proc. International Conference on Computer Languages, pp. 90–101 (1998)

    Google Scholar 

  27. Jones, G., Sheeran, M.: Circuit design in Ruby. In: Staunstrup, J. (ed.) Formal Methods for VLSI Design, pp. 13–70. North-Holland, Amsterdam (1990)

    Google Scholar 

  28. Lamport, L.: The Temporal Logic of Actions. ACM TOPLAS 16(3), 872–923 (1994)

    Article  Google Scholar 

  29. Lamport, L.: Specifying Systems — The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading, Massachusetts (2002)

    Google Scholar 

  30. Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  31. Mycroft, A., Sharp, R.: A Statically Allocated Parallel Functional Language. Automata, Languages and Programming, pp. 37–48 (2000)

    Google Scholar 

  32. Mycroft, A., Sharp, R.: Hardware/Software Co-Design Using Functional Languages. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 236–251. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  33. 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. 2391, pp. 184–203. Springer, Heidelberg (2002)

    Google Scholar 

  34. Vasconcelos, P.B.: Cost Inference and Analysis for Recursive Functional Programs. PhD thesis, University of St Andrews (in preparation)

    Google Scholar 

  35. Vasconcelos, P.B., Hammond, K.: Inferring Costs for Recursive, Polymorphic and Higher-Order Functional Programs. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 86–101. Springer, Heidelberg (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of St Andrews, St Andrews, Scotland

    Kevin Hammond

  2. Dept. of Mathematics and Computer Science, Heriot-Watt University, Edinburgh, Scotland

    Gudmund Grov, Greg Michaelson & Andrew Ireland

Authors
  1. Kevin Hammond
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gudmund Grov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Greg Michaelson
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andrew Ireland
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Zoltán Horváth Viktória Zsók Andrew Butterfield

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hammond, K., Grov, G., Michaelson, G., Ireland, A. (2007). Low-Level Programming in Hume: An Exploration of the HW-Hume Level. In: Horváth, Z., Zsók, V., Butterfield, A. (eds) Implementation and Application of Functional Languages. IFL 2006. Lecture Notes in Computer Science, vol 4449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74130-5_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74130-5_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74129-9

  • Online ISBN: 978-3-540-74130-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation