A principled approach to operating system construction in Haskell Export

@inproceedings{citeulike:333537, abstract = {We describe a monadic interface to low-level hardware features that is a suitable basis for building operating systems in Haskell. The interface includes primitives for controlling memory management hardware, user-mode process execution, and low-level device I/O. The interface enforces memory safety in nearly all circumstances. Its behavior is specified in part by formal assertions written in a programming logic called P-Logic. The interface has been implemented on bare IA32 hardware using the Glasgow Haskell Compiler (GHC) runtime system. We show how a variety of simple O/S kernels can be constructed on top of the interface, including a simple separation kernel and a demonstration system in which the kernel, window system, and all device drivers are written in Haskell.}, address = {New York, NY, USA}, author = {Hallgren, Thomas and Jones, Mark P. and Leslie, Rebekah and Tolmach, Andrew}, booktitle = {ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming}, citeulike-article-id = {333537}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1086365.1086380}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1086365.1086380}, doi = {10.1145/1086365.1086380}, isbn = {1595930647}, keywords = {functional-programming, haskell, monads, operating-systems, programatica, side-effects, verification}, pages = {116--128}, posted-at = {2005-09-28 09:22:49}, priority = {0}, publisher = {ACM Press}, title = {A principled approach to operating system construction in Haskell}, url = {http://dx.doi.org/10.1145/1086365.1086380}, year = {2005} }

TY - CONF ID - citeulike:333537 L3 - citeulike-article-id:333537 N2 - We describe a monadic interface to low-level hardware features that is a suitable basis for building operating systems in Haskell. The interface includes primitives for controlling memory management hardware, user-mode process execution, and low-level device I/O. The interface enforces memory safety in nearly all circumstances. Its behavior is specified in part by formal assertions written in a programming logic called P-Logic. The interface has been implemented on bare IA32 hardware using the Glasgow Haskell Compiler (GHC) runtime system. We show how a variety of simple O/S kernels can be constructed on top of the interface, including a simple separation kernel and a demonstration system in which the kernel, window system, and all device drivers are written in Haskell. SN - 1595930647 AD - New York, NY, USA EP - 128 TI - A principled approach to operating system construction in Haskell PB - ACM Press T2 - ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming SP - 116 KW - functional-programming KW - haskell KW - monads KW - operating-systems KW - programatica KW - side-effects KW - verification AU - Hallgren, Thomas AU - Jones, Mark AU - Leslie, Rebekah AU - Tolmach, Andrew PY - 2005/// UR - http://dx.doi.org/10.1145/1086365.1086380 ER -