Hume Language – Papers on Hume

[2008] | [2007] | [2006] | [2005] | [2004] | [2003] | [2002] | [2001] | [2000]

2008

Preserving Coordination Properties when Transforming Concurrent System Components
Gudmund Grov, Robert Pointon, Greg Michaelson, and Andrew Ireland. Coordination Models, Languages and Applications Track of the 23rd Annual ACM Symposium on Applied Computing, 2008. To appear.
Costing by Construction: Compositional Design and Verification of Embedded Applications using the Hume Software Development Methodology
Norman Scaife, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, and Jocelyn Serot. 2008 In preparation.

2007

Towards Resource-Certified Software: A Formal Cost Model for Time and its Application to an Image-Processing Example
Armelle Bonenfant, Zezhi Chen, Kevin Hammond, Greg Michaelson, Andy Wallace, and Iain Wallace. ACM Symposium on Applied Computing (SAC '07), Seoul, Korea, March 11-15, Seoul, Korea, 2007. To appear.
Worst-Case Execution Times for a Purely Functional Language
Armelle Bonenfant, Christian Ferdinand, Kevin Hammond, and Reinhold Heckmann. Proc. Implementation of Functional Languages (IFL 2006), Lecture Notes in Computer Science 4449, Springer, 2007. To appear
Using Mean-Shift Tracking Algorithms for Real-Time Tracking of Moving Images on an Autonomous Vehicle Testbed Platform
Benjamin Gorry, Zezhi Chen, Kevin Hammond, Andy Wallace, and Greg Michaelson. IRMA 2007, International Conference on Intelligent Robotics and Manufacturing Automation, Venice, Italy, November 23-25, 2007, Proceedings of the World Academy of Science, Engineering and Technology 25, World Academy of Science, Engineering and Technology, 2007, pp. 356--361.
A Formal Account of Hume Scheduling
Gudmund Grov. Heriot-Watt Technical Report HW-MACS-TR-0052, 2007.
Towards a Box Calculus for Hierarchical Hume
Gudmund Grov and Greg Michaelson. Trends in Functional Programming, Marco T. Morazan (ed.) : 8, Intellect, 2007, pp. 71--88.
Formal Verification of Concurrent Scheduling Strategies using TLA
Gudmund Grov, Greg Michaelson, and Andrew Ireland. 3rd IEEE International Workshop on Scheduling and Resource Management for Parallel and Distributed Systems, IEEE Catalog Number, IEEE, 2007.
Preserving Coordination Properties when Transforming Concurrent System Components
Gudmund Grov, Robert Pointon, Greg Michaelson, and Andrew Ireland. Heriot-Watt Technical Report HW-MACS-TR-0054, 2007.
On Hume Scheduling
Gudmund Grov, Robert Pointon, Greg Michaelson, and Andrew Ireland. Heriot-Watt Technical Report HW-MACS-TR-0046, 2007.
Low-Level Programming in Hume: an Exploration of the HW-Hume Level
Kevin Hammond, Gudmund Grov, Greg Michaelson, and Andrew Ireland. Proc. Implementation of Functional Languages (IFL 2006), Lecture Notes in Computer Science 4449, Springer, 2007. To appear.
Automatic Amortised Worst-Case Execution Time Analysis
Christoph A. Herrmann, Armelle Bonenfant, Kevin Hammond, Steffen Jost, Hans-Wolfgang Loidl, and Robert Pointon. 7th Int'l Workshop on Worst-Case Execution Time (WCET) Analysis, Proceedings, Pisa, Italy, July 3, 2007, 2007, pp. 13--18.
HW-Hume in Isabelle
Chunxu Liu and Greg Michaelson. Draft Proceedings of 19th International Symposium on Implementation and Application of Functional Languages, O. Chitil (ed.) , 2007, pp. 366--381.
Programming Embedded Lift Control Logic in Hume
Gergely Patai and Péter Hanák. Proc. Implementation of Functional Languages (IFL 2006), Lecture Notes in Computer Science 4449, Springer, 2007. To appear.
Embedded Functional Programming in Hume
Gergely Patai and Péter Hanák. IASTED on Software Engineering, ACTA Press, Innsbruck, Austria, 2007, pp. 328-333.
Abstract: Embedded systems represent a rapidly growing branch of information technology, characterised by the need for increased dependability, timeliness and efficiency. While functional languages allow developers to produce highly reliable and maintainable code, they ignore the aspect of time, and their efficiency is inferior to those of low-level languages currently dominating this field. Hume is a novel hybrid language that combines the functional paradigm with ideas from hardware design. It focuses on producing time- and space-constrained code while keeping the benefits of programming on a high level. This paper describes the development of a lift control simulation in Hume running on low-performance embedded hardware platforms, including the process of porting the code to these platforms.

2006

A Verified Staged Interpreter is a Verified Compiler: Multi-stage Programming with Dependent Types
Edwin Brady and Kevin Hammond. Generative Programming and Component Engineering, 5th International Conference (GPCE 2006), Portland, Portland, Oregon, USA, October 22-26, Stan Jarzabek, Douglas C. Schmidt, and Todd L. Veldhuizen (eds.) , ACM, 2006, pp. 111--120.
Programming Embedded Systems in Functional Languages
Patai Gergely. Master's Thesis. Budapest University of Technology and Economics, 2006.
Verifying Temporal Properties in HW-Hume
Gudmund Grov, Andrew Ireland, Greg Michaelson, and Kevin Hammond. Heriot-Watt Technical Report HW-MACS-TR-0037, 2006.
Exploiting Purely Functional Programming to Obtain Bounded Resource Behaviour: the Hume Approach
Kevin Hammond. First Central European Summer School, CEFP 2005, Budapest, Hungary, July 4-15, 2005, Revised Selected Lectures, Zoltán Horváth (ed.) : Lecture Notes in Computer Science 4164, Springer-Verlag, 2006, pp. 100-134.
The EmBounded project (project paper)
Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn Sérot, and Andy Wallace. Proc. 6th Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005, Trends in Functional Programming 6, Intellect, 2006. To appear.
Towards Formally Verifiable Resource Bounds for Real-Time Embedded Systems
Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hoffmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace. ACM SIGBED Review--- Special issues on Workshop on Innovative Techniques for Certification of Embedded Systems 2006 (ITCES06) 3 (4), October 2006, pp. 27--36.
Abstract: This paper describes ongoing work aimed at the construction of formal cost models and analyses that are capable of producing verifiable guarantees of resource usage (space, time and ultimately power consumption) in the context of real-time embedded systems. Our work is conducted in terms of the domain-specific language Hume, a language that combines functional programming for computations with finite-state automata for specifying reactive systems. We describe an approach in which high-level information derived from source-code analysis can be combined with worst-case execution time information obtained from abstract interpretation of low-level binary code. This abstract interpretation on the machine-code level is capable of dealing with complex architectural effects including cache and pipeline properties in an accurate way.
Towards Formally Verifiable WCET Analysis for a Functional Programming Language
Kevin Hammond, Christian Ferdinand, Reinhold Heckmann, Roy Dyckhoff, Martin Hofman, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Robert Pointon, Norman Scaife, Jocelyn Sérot, and Andy Wallace. 6th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Frank Mueller (ed.) : Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, 2006.
Abstract: This paper describes ongoing work aimed at the construction of formal cost models and analyses to yield verifiable guarantees of resource usage in the context of real-time embedded systems. Our work is conducted in terms of the domain-specific language Hume, a language that combines functional programming for computations with finitestate automata for specifying reactive systems. We outline an approach in which high-level information derived from source-code analysis can be combined with worst-case execution time information obtained from high quality abstract interpretation of low-level binary code.
Towards Hardware/Software Codesign: Exploring the HW-HumeLevel
Kevin Hammond, Greg Michaelson, and Gudmond Grov. Draft proceedings 18th International Symposium on Implementation and Application of Functional Programs, Budapest, Hungary, September 2006, Z. Horvath and V. Zsok (eds.) , 2006, pp. 99--114.
Programming Reactive Systems in Hume (Extended Abstract)
Kevin Hammond, Greg Michaelson, and Meng Sun. Proceedings of Symposium on Trends in Functional Programming, University of Nottingham, UK, 19-21 April, 2006, H. Nilsson and M van Eekling (eds.) : Trends in Functional Programming, Intellect, 2006. To appear
Bounded Space Programming using Finite State Machines and Recursive Functions: the Hume Approach
Kevin Hammond, Greg Michaelson, and Pedro Vasconcelos. ACM Transactions on Software Engineering Methodology (TOSEM), 2006. Submitted
Recursion, Iteration and Hume Scheduling
Greg Michaelson, Robert Pointon, Gudmond Grove, and Andrew Ireland. Proceedings of Symposium on Trends in Functional Programming, University of Nottingham, UK, 19-21 April, 2006, H. Nilsson and M van Eekling (eds.) : Trends in Functional Programming, Intellect, 2006. To appear
Toward Resource Certified Image Processing Software
Greg Michaelson, Andy Wallace, Kevin Hammond, Iain Wallace, Armelle Bonenfant, and Zezhi Chen. Systems Engineering for Autonomous Systems Defence Technology Centre (SEAS DTC), Annual Technical Conference, July 2006, Edinburgh, Conference Proceedings, Edinburgh, UK MoD, 2006, pp. A15.

2005

Verifying the correctness of Hume programs: an approach combining deductive and algorithmic reasoning.
Gudmund Grov. 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), November 7-11, 2005, Long Beach, CA, USA, David F. Redmiles, Thomas Ellman, and Andrea Zisman (eds.) , ACM, 2005, pp. 444--447.
Model Checking HW-Hume
Gudmund Grov, Andrew Ireland, and Greg Michaelson. Heriot-Watt Technical Report HW-MACS-TR-0032, 2005.
Is it Time for Real-Time Functional Programming?
Kevin Hammond. Trends in Functional Programming, Volume 4, Stephen Gilmore (ed.) : Trends in Functional Programming 4, Intellect, 2005, pp. 1-14.
The EmBounded project (project paper)
Kevin Hammond, Roy Dyckhoff, Christian Ferdinand, Reinhold Heckmann, Martin Hofmann, Steffen Jost, Hans-Wolfgang Loidl, Greg Michaelson, Jocelyn Sérot, and Andy Wallace. Proc. 6th Symposium on Trends in Functional Programming (TFP 2005), Tallinn, Estonia, 23-24 September 2005, Institute of Cybernetics, 2005, pp. 220-235. Online
Towards a Hume IDE
Chunxu Liu and Greg Michaelson. Draft Proceedings of 6th Symposium on Trends in Functional programming, Institute of Cybernetics, Tallinn, Estonia, September 2005, M. van Eekling and K. Hammond (eds.) , 2005, pp. 355--369.
FSM-Hume is Finite State
Greg Michaelson, Kevin Hammond, and Jocelyn Sérot. Trends in Functional Programming, Volume 4, Stephen Gilmore (ed.) : Trends in Functional Programming 4, Intellect, 2005, pp. 19-28.

2004

Model Checking HW-Hume
Gudmund Grov, Andrew Ireland, and Greg Michaelson. Draft Proceedings of 5th Symposium on Trends in Functional Programming, Ludwig-Maximillian's Universitat, Munich, Germany, November 2004, Hans-Wolfgang Loidl (ed.) , 2004, pp. 33--48.
Translating Hume to Java
Chunxu Liu and Greg Michaelson. Draft Proceedings of 5th Symposium on Trends in Functional Programming, Ludwig-Maximillian's Universitat, Munich, Germany, November 2004, Hans-Wolfgang Loidl (ed.) , 2004, pp. 113--128.
FSM-Hume: programming resource-limited systems using bounded automata.
Greg Michaelson, Kevin Hammond, and Jocelyn Sérot. Proceedings of the 2004 ACM Symposium on Applied Computing (SAC), Nicosia, Cyprus, March 14-17, 2004, Hisham Haddad, Andrea Omicini, Roger L. Wainwright, and Lorie M. Liebrock (eds.) , 2004, pp. 1455-1461.
Abstract: Hume is a novel domain-specific programming language targeting resource-bounded computations, such as real-time embedded systems or mobile code. It is based on generalised concurrent automata, controlled by transitions characterised by pattern matching on inputs and (recursive) function generation on outputs. This paper discusses trade-offs between expressibility and decidability in the design of FSM-Hume, a subset of Hume (or Hume layer) based on generalised linear bounded automata with statically determinable time and space use. We illustrate our approach with reference to a simple real-time simulation of a line-following autonomous vehicle controlled by video camera input.

2003

The Finite State-ness of FSM-Hume
Proceedings of Symposium on Trends in Functional Programming, Edinburgh, Scotland, September 2003, Edinburgh, Scotland, 2003.
Abstract: Hume is a domain-specific programming language targeting resource-bounded computations, such as real-time embedded systems. It is novel in being based on generalised concurrent bounded automata, controlled by transitions characterised by pattern matching on inputs and recursive function generation of outputs. FSM-Hume is a strict finite state subset of Hume, where symbols are constrained to fixed size types and transition functions are non-recursive. Here we discuss the design of FSM-Hume and show that it is indeed classically finite state.
An Abstract Machine Implementation for Hume
Kevin Hammond. 2003
Abstract: This unpublished paper gives fuller details of the prototype Hume Abstract Machine (pHAM) implementation.
Hume: A Domain-Specific Language for Real-Time Embedded Systems.
Kevin Hammond and Greg Michaelson. Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings, Frank Pfenning and Yannis Smaragdakis (eds.) : Lecture Notes in Computer Science 2830, Springer, 2003, pp. 37-56.
The Design of Hume: A High-Level Language for the Real-Time Embedded Systems Domain.
Kevin Hammond and Greg Michaelson. Domain-Specific Program Generation: International Seminar, Dagstuhl Castle, Germany, March 23-28, 2003, Revised Papers, Christian Lengauer, Don S. Batory, Charles Consel, and Martin Odersky (eds.) : Lecture Notes in Computer Science 3016, Springer, 2003, pp. 127-142.
Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs.
Pedro B. Vasconcelos and Kevin Hammond. Implementation of Functional Languages, 15th International Workshop, IFL 2003, Edinburgh, UK, September 8-11, 2003, Revised Papers, Philip W. Trinder, Greg Michaelson, and Ricardo Pena (eds.) : Lecture Notes in Computer Science 3145, Springer, 2003, pp. 86-101.

2002

Predictable Space Behaviour in FSM-Hume
Kevin Hammond and Greg Michaelson. Implementation of Functional Languages: 14th International Workshop, IFL 2002, Madrid, Spain, September 16-18, 2002, Revised Selected Papers, Ricardo Peña and Thomas Arts (eds.) : Lecture Notes in Computer Science 2670, Springer, 2002, pp. 1-16.
Cost Analysis Using Automatic Size and Time Inference
Álvaro J. Rebón Portillo, Kevin Hammond, Hans-Wolfgang Loidl, and Pedro B. Vasconcelos. Implementation of Functional Languages, 14th International Workshop, IFL 2002, Madrid, Spain, September 16-18, 2002, Revised Selected Papers, Ricardo Pena and Thomas Arts (eds.) : Lecture Notes in Computer Science 2670, Springer, 2002, pp. 232-248.

2001

The Dynamic Properties of Hume: a Functionally-Based Concurrent Language with Bounded Time and Space Behaviour
Kevin Hammond. Implementation of Functional Languages : 12th International Workshop, IFL 2000 Aachen, Germany, September 4-7, 2000, Selected Papers, Lecture Notes in Computer Science 2011, Springer, 2001, pp. 122.
Abstract: This paper provides a self-contained formal description of the dynamic properties of Hume, a novel functionally-based concurrent language that aims to target space- and time-critical systems such as safety-critical, embedded and real-time systems. The language is designed to support rigorous cost and space analyses, whilst providing a high level of ion including polymorphic type inference, automatic memory management, higher-order functions, exception-handling and a good range of primitive types.
The Dynamic Properties of Hume: A Functionally-Based Concurrent Language with Bounded Time and Space Behaviour
Kevin Hammond. Implementation of Functional Languages : 12th International Workshop, IFL 2000 Aachen, Germany, September 4-7, 2000, Selected Papers, Lecture Notes in Computer Science 2011, Springer, 2001, pp. 122.
Abstract: This paper provides a self-contained formal description of the dynamic properties of Hume, a novel functionally-based concurrent language that aims to target space- and time-critical systems such as safety-critical, embedded and real-time systems. The language is designed to support rigorous cost and space analyses, whilst providing a high level of ion including polymorphic type inference, automatic memory management, higher-order functions, exception-handling and a good range of primitive types.

2000

Hume: a Concurrent Language with Bounded Time and Space Behaviour
Kevin Hammond. Proc. 7th IEEE International Conference on Electronic Control Systems (ICECS 2K), Lebanon, 2000, pp. 407-411.
Constraints on Recursion in the Hume Programming Language
Greg Michaelson. Draft Proc. IFL 2000 -- Intl. Workshop on Implementation of Functional Languages, Aachen, Germany, 2000.
Hume: a Functionally-Inspired Language for Safety-Critical Systems
Greg Michaelson and Kevin Hammond. Draft proceedings from the 2nd Scottish Functional Programming Workshop (SFP00), University of St Andrews, Scotland, July 26th to 28th, 2000, St Andrews, Scotland, Trends in Functional Programming 2, 2000.

This page was last modified on Monday 11 February 2008 11:49:23. This site is maintained by Robert Rothenberg (r r at cs dot st - andrews dot ac dot uk).