@article{CheapThreads,
  author =       "William L. Harrison and Adam Procter",
  title =        "Cheap (But Functional) Threads",
  journal =      "Higher Order and Symbolic Computation (accepted for publication)",
  note = {Draft version},
  year = 2015,                  
  abstract = "This article demonstrates how a powerful and expressive abstraction 
from concurrency theory plays a dual role as a programming tool 
for concurrent applications and as a foundation for their verification.
This abstraction---monads of resumptions expressed using monad 
transformers---is \emph{cheap}: it is easy to understand, easy to 
implement, and easy to reason about.
We illustrate the expressiveness of the resumption monad with the 
construction of an exemplary multitasking operating system kernel 
with process forking, preemption, message passing, and 
synchronization constructs in the pure functional programming 
language Haskell.
Because resumption computations are stream-like structures, reasoning 
about this kernel may be posed as reasoning about streams, a problem 
which is well-understood. And, as an example, this article 
illustrates how a liveness property---fairness---is proven and 
especially how the resumption-monadic structure promotes such 
verifications.",
  url_Paper = "https://harrisonwl.github.io/assets/papers/hosc-cheapthreads.pdf",
}

{"_id":"ehwoLgebqb27uPLv4","bibbaseid":"harrison-procter-cheapbutfunctionalthreads-2015","downloads":4,"creationDate":"2017-11-17T18:00:21.779Z","title":"Cheap (But Functional) Threads","author_short":["Harrison, W. L.","Procter, A."],"year":2015,"bibtype":"article","biburl":"https://harrisonwl.github.io/assets/bibliography/harrison.bib","bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["William","L."],"propositions":[],"lastnames":["Harrison"],"suffixes":[]},{"firstnames":["Adam"],"propositions":[],"lastnames":["Procter"],"suffixes":[]}],"title":"Cheap (But Functional) Threads","journal":"Higher Order and Symbolic Computation (accepted for publication)","note":"Draft version","year":"2015","abstract":"This article demonstrates how a powerful and expressive abstraction from concurrency theory plays a dual role as a programming tool for concurrent applications and as a foundation for their verification. This abstraction—monads of resumptions expressed using monad transformers—is \\emphcheap: it is easy to understand, easy to implement, and easy to reason about. We illustrate the expressiveness of the resumption monad with the construction of an exemplary multitasking operating system kernel with process forking, preemption, message passing, and synchronization constructs in the pure functional programming language Haskell. Because resumption computations are stream-like structures, reasoning about this kernel may be posed as reasoning about streams, a problem which is well-understood. And, as an example, this article illustrates how a liveness property—fairness—is proven and especially how the resumption-monadic structure promotes such verifications.","url_paper":"https://harrisonwl.github.io/assets/papers/hosc-cheapthreads.pdf","bibtex":"@article{CheapThreads,\n author = \"William L. Harrison and Adam Procter\",\n title = \"Cheap (But Functional) Threads\",\n journal = \"Higher Order and Symbolic Computation (accepted for publication)\",\n note = {Draft version},\n year = 2015, \n abstract = \"This article demonstrates how a powerful and expressive abstraction \nfrom concurrency theory plays a dual role as a programming tool \nfor concurrent applications and as a foundation for their verification.\nThis abstraction---monads of resumptions expressed using monad \ntransformers---is \\emph{cheap}: it is easy to understand, easy to \nimplement, and easy to reason about.\nWe illustrate the expressiveness of the resumption monad with the \nconstruction of an exemplary multitasking operating system kernel \nwith process forking, preemption, message passing, and \nsynchronization constructs in the pure functional programming \nlanguage Haskell.\nBecause resumption computations are stream-like structures, reasoning \nabout this kernel may be posed as reasoning about streams, a problem \nwhich is well-understood. And, as an example, this article \nillustrates how a liveness property---fairness---is proven and \nespecially how the resumption-monadic structure promotes such \nverifications.\",\n url_Paper = \"https://harrisonwl.github.io/assets/papers/hosc-cheapthreads.pdf\",\n}\n\n","author_short":["Harrison, W. L.","Procter, A."],"key":"CheapThreads","id":"CheapThreads","bibbaseid":"harrison-procter-cheapbutfunctionalthreads-2015","role":"author","urls":{" paper":"https://harrisonwl.github.io/assets/papers/hosc-cheapthreads.pdf"},"metadata":{"authorlinks":{"harrison, w":"https://harrisonwl.github.io/etc/publications.html"}},"downloads":4},"search_terms":["cheap","functional","threads","harrison","procter"],"keywords":[],"authorIDs":["5dc475579b60c2df010000fb","5dee581feaaee4df01000254","5df9dbe338a7afde010000b8","5e03c9676d2066de01000013","5e2b8df4f92538df01000009","5e55f36cc2c8a2df010000f1","5e64fd0d5fc0b7de010000d4","BPp6pLGb3wvE8tPNi","GrcodozaBpTrw2nXH","NmXf49aeDyLF3AL8F","a66s2jJ42S97qQxnX","iCiuqX2A39oLpzRv9","njB2ZmsnMejPsL7oC","uBWQddfiBuSzTqKrJ","xkL56M792TvXx8Hef"],"dataSources":["wAeScLDKnpPTHdYwg","uCveoExKMHQNZnZCp"]}