Towards Machine-Verified Proofs for I/O
| Autor: | Dowse, M., Butterfield, A., Eekelen, M.C.J.D. van, Mol, M.J. de, Plasmeijer, M.J., Grelck, C., Huch, F. |
|---|---|
| Přispěvatelé: | Grelck, C., Huch, F. |
| Rok vydání: | 2004 |
| Předmět: | |
| Zdroj: | Grelck, C.; Huch, F. (ed.), Proceedings Implementation and Application of Functional Languages, 16th International Workshop, IFL'04, 469-480. [S.l.] : Christian-Albrechts-Universitaet zu Kiel STARTPAGE=469;ENDPAGE=480;TITLE=Grelck, C.; Huch, F. (ed.), Proceedings Implementation and Application of Functional Languages, 16th International Workshop, IFL'04 Grelck, C.; Huch, F. (ed.), Proceedings Implementation and Application of Functional Languages, 16th International Workshop, IFL'04, pp. 469-480 |
| Popis: | Contains fulltext : 60288.pdf (Author’s version preprint ) (Open Access) In functional languages, the shape of the external world affects both our understanding of I/O and how we would wish to have I/O expressed. This paper takes the first tentative steps at examining the consequences of using an explicit model of the external world-state when reasoning (using tool-support) about the behaviour of lazy functional programs. We construct a file-system model and develop a monadic language which lets us structure I/O. Two proofs are then performed regarding the observable effect of real-world functional I/O, and it is shown how properties of the file-system lend themselves naturally to the modelling of concurrent behaviour on a single, global state. All proofs in this paper were machine-verified using the Sparkle proof-assistant. , 16th International Workshop, IFL'04, Luebeck, Germany, September 8-10, 2004 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|