Proof Tool Support for Explicit Strictness

In programs written in lazy functional languages such as for example Clean and Haskell, the programmer can choose freely whether particular subexpressions will be evaluated lazily (the default) or strictly (must be specified explicitly). It is widely known that this choice affects program behavior, resource consumption and semantics in several ways. However, not much experience is available about the impact on logical program properties and formal reasoning. This paper aims to give a better understanding of the concept of explicit strictness. The impact of explicit strictness on formal reasoning will be investigated. It will be shown that this impact is bigger than expected and that tool support is needed for formal reasoning in the context of explicit strictness. We introduce the various ways in which strictness specific support is offered by the proof assistant Sparkle.

• Type: Conference
• Year: 2005
• Where: IFL
• Authors: Marko C. J. D. van Eekelen, Maarten de Mol
• Keywords: Explicit Strictness, Formal Reasoning, IFL 2005, Lazy Functional Languages