Functional Programming and Input/Output

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 Also 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. Graduate Students And Researchers Will Gain Much From Reading This Book.