Reasoning about deterministic concurrent functional I/O

Autor:	Dowse, M., Butterfield, A., Eekelen, M.C.J.D. van, Grelck, C., Huch, F., Michaelson, G.J., Trinder, Ph.
Přispěvatelé:	Grelck, C., Huch, F., Michaelson, G.J., Trinder, Ph.
Předmět:	Input/output Functional programming business.industry Computer science Programming language Concurrency Metalanguage computer.software_genre Software Technology Computer Science::Programming Languages Artificial intelligence State (computer science) business computer Security of Systems
Zdroj:	Scopus-Elsevier Grelck, C.; Huch, F.; Michaelson, G.J. (ed.), Implementation and Application of Functional Languages : 16th International Workshop, IFL 2004 Lübeck, Germany, September 8-10, 2004, Revised Selected Papers, 469-480. Berlin : Springer STARTPAGE=469;ENDPAGE=480;ISSN=0302-9743;TITLE=Grelck, C.; Huch, F.; Michaelson, G.J. (ed.), Implementation and Application of Functional Languages : 16th International Workshop, IFL 2004 Lübeck, Germany, September 8-10, 2004, Revised Selected Papers Implementation and Application of Functional Languages ISBN: 9783540260943 IFL Grelck, C.; Huch, F.; Michaelson, G.J. (ed.), Implementation and Application of Functional Languages : 16th International Workshop, IFL 2004 Lübeck, Germany, September 8-10, 2004, Revised Selected Papers, LNCS, pp. 469-480
ISSN:	0302-9743
Popis:	This paper develops a language for reasoning about concurrent functional I/O. We assume that the API is specified as state-transformers on a single world state. We then prove that under certain conditions evaluation in this language is deterministic, and give some examples. All properties were machine-verified using the Sparkle proof-assistant and using Core-Clean as a meta-language.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::571083597748b15943c04900e9960832 http://www.scopus.com/inward/record.url?eid=2-s2.0-24944540835&partnerID=MN8TOARS Zobrazit plný text záznamu