A useful bounded resource functional language

Abstract

Real-time software, particularly that used in embedded systems, has unique resource and verification requirements. While embedded software may not have great need for processor and memory resources, the need to prove that computations are performed correctly and within hard time and space constraints is very great. Improvements in hardware and compiler technology mean that functional programming languages are increasingly practical for embedded situations. We present a functional programming language, CA, built on catamorphisms instead of general recursion, intended for use in static analysis. CA is not Turing-complete - every program must terminate-but it still provides an excellent framework for building static analysis techniques. Catamorphisms are a general tool which encompass bounded iteration, and allow to traverse any algebraic data structure. We discuss the computational properties of this language, as well as provide a framework for future work in static analysis. © Springer-Verlag Berlin Heidelberg 2008.