Proving Make Correct: I/O Proofs in Haskell and Clean

  • Malcolm Dowse
  • Glenn Strong
  • Andrew Butterfield
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2670)


This paper discusses reasoning about I/O operations in the languages Haskell and Clean and makes some observations about proving properties of programs which perform significant I/O. We developed a model of the I/O system and produced some techniques to reason about the behaviour of programs run in the model. We then used those techniques to prove some properties of a program based on the standard make tool. We consider the I/O systems of both languages from a program proving perspective, and note some similarities in the overall structure of the proofs. A set of operators for assisting in the reasoning process are defined, and we then draw some conclusions concerning reasoning about the effect of functional programs on the outside world, give some suggestions for techniques and discuss future work.


Formal Proof Trinity College Concurrent Process Dependency Tree Functional Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andrew Butterfield and Glenn Strong. Comparing i/o proofs in three programming paradigms: a baseline. Technical Report TCD-CS-2001-28, University of Dublin, Trinity College, Department of Computer Science, August 2001.Google Scholar
  2. 2.
    Andrew Butterfield and Glenn Strong. Proving correctness of programs with i/o — a paradigm comparison. In Markus Mohnen Thomas Arts, editor, Proceedings of the 13th International Workshop, IFL 2001, number LNCSn2312 in Lecture Notes in Computer Science, pages 72–87. Springer-Verlag, 2001.Google Scholar
  3. 3.
    Richard M. Stallman and Roland McGrath. GNU Make: A Program for Directing Recompilation, for Version 3.79. Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA, Tel: (617) 876-3296, USA, 2000.Google Scholar
  4. 4.
    Malcolm Dowse, Glenn Strong, and Andrew Butterfield. Proving “make” correct: I/o proofs in two functional languages. Technical Report TCDCS-2003-03, Trinity College, Dublin, 2003. Scholar
  5. 5.
    Paul Hudak, Simon L. Peyton Jones, and Philip Wadler (editors). Report on the programming language haskell, a non-strict purely functional language (version 1.2). SIGPLAN Notices, Mar, 1992.Google Scholar
  6. 6.
    Stuart I. Feldman. Make-a program for maintaining computer programs. Software-Practice and Experience, 9(4):255–65, 1979.zbMATHCrossRefGoogle Scholar
  7. 7.
    Maarten de Mol, Marko van Eekelen, and Rinus Plasmeijer. Sparkle: A functional theorem prover. In Markus Mohnen Thomas Arts, editor, Proceedings of the 13th International Workshop, IFL2001, number LNCS2312 in Lecture Notes in Computer Science, page 55. Springer-Verlag, 2001.Google Scholar
  8. 8.
    Rinus Plasmeijer and Marko van Eekelen. Concurrent clean version 2.0 language report., December 2001.
  9. 9.
    Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6(6):579–612, 1996.zbMATHMathSciNetGoogle Scholar
  10. 10.
    Philip Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi: Proceedings of the 1992 Marktoberdorf International Summer School. Springer-Verlag, 1993.Google Scholar
  11. 11.
    He Jifeng, C. A. R. Hoare, M. Fränzle, M. Müller-Ulm, E.-R. Olderog, M. Schenke, A. P. Ravn, and H. Rischel. Provably correct systems. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real Time and Fault Tolerant Systems, volume 863, pages 288–335. Springer-Verlag, 1994.Google Scholar
  12. 12.
    Andrew D. Gordon. Functional Programming and Input/Output. PhD thesis, University of Cambridge, August 1992.Google Scholar
  13. 13.
    Mícheál Mac an Airchinnigh. Conceptual Models and Computing. PhD thesis, University of Dublin, Trinity College, Department of Computer Science, 1990.Google Scholar
  14. 14.
    Arthur Hughes. Elements of an Operator Calculus. PhD thesis, University of Dublin, Trinity College, Department of Computer Science, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Malcolm Dowse
    • 1
  • Glenn Strong
    • 1
  • Andrew Butterfield
    • 1
  1. 1.Trinity CollegeDublin UniversityDublin

Personalised recommendations