TY  - BOOK
AU  - Gordon,Andrew D.
TI  - Functional programming and input/output / 
T2  - Distinguished dissertations in computer science
SN  - 0521471036
U1  - 005.711   22
PY  - 1994///
CY  - Cambridge [England] ; ,  New York : 
PB  -  Cambridge University Press, 
KW  - Functional programming (Computer science)
KW  - Computer input-output equipment
N1  - Includes bibliographical references (p. 137-147) and indexes; Introduction -- A calculus of recursive types -- A metalanguage for semantics -- Operational precongruence -- Theory of the metalanguage -- An operational theory of functional programming -- Four mechanisms for teletype I/O -- Monadic I/O -- Conclusion
N2  - A common attraction to functional programming is the ease with which proofs can be given of program properties. A common disappointment with functional programming is the difficulty of expressing input/output (I/O), while at the same time being able to verify programs. Here, the author shows how a theory of functional programming can be smoothly extended to admit both an operational semantics for functional I/O and verification of programs engaged in I/O. He obtains, for the first time, operational semantics for the three most widely implemented I/O mechanisms for lazy languages, and proves that the three are equivalent in expressive power. He develops semantics for a form of monadic I/O and verifies a simple programming example. These theories of functional I/O are based on an entirely operational theory of functional programming, developed using Abramsky's 'applicative bisimulation'
ER  -