var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Fharrisonwl.github.io%2Fassets%2Fbibliography%2Fharrison.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Fharrisonwl.github.io%2Fassets%2Fbibliography%2Fharrison.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Fharrisonwl.github.io%2Fassets%2Fbibliography%2Fharrison.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2024\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Temporal Staging for Correct-by-Construction Cryptographic Hardware.\n \n \n \n \n\n\n \n Forman, Y.; and Harrison, W. L.\n\n\n \n\n\n\n In Rapid Systems Prototyping (RSP24), 2024. \n \n\n\n\n
\n\n\n\n \n \n \"Temporal paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison24,\n  title = {Temporal Staging for Correct-by-Construction Cryptographic Hardware},\n  author = {Forman, Yakir and Harrison, William L.},\n  booktitle = {Rapid Systems Prototyping (RSP24)},\n  year = {2024},\n  abstract = {\n There is a conceptual divide between the ways cryptographic algorithms are defined (i.e., informal imperative pseudocode) and commodity hardware design languages (e.g., Verilog). How does one even begin to compare a pseudocode to an HDL design that purports to implement it in hardware? Bridging this divide requires substantial manual intervention and, consequently, ``shrinking the divide'' can drastically reduce the cost of high-assurance cryptographic hardware by reducing the cost of formal verification. We present a correct-by-construction methodology for the functional hardware design language, ReWire, in which a reference cryptographic algorithm is transformed into a provably correct hardware design with a program transformation called temporal staging. We illustrate this methodology with case studies including one for the BLAKE2b cryptographic hash function. Because the reference algorithm, the temporal staging transformation, and the resulting implementation are all expressed in ReWire, formal verification can proceed immediately via a published ReWire semantics.\n},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/rsp24.pdf",\n}\n\n                  \n
\n
\n\n\n
\n There is a conceptual divide between the ways cryptographic algorithms are defined (i.e., informal imperative pseudocode) and commodity hardware design languages (e.g., Verilog). How does one even begin to compare a pseudocode to an HDL design that purports to implement it in hardware? Bridging this divide requires substantial manual intervention and, consequently, ``shrinking the divide'' can drastically reduce the cost of high-assurance cryptographic hardware by reducing the cost of formal verification. We present a correct-by-construction methodology for the functional hardware design language, ReWire, in which a reference cryptographic algorithm is transformed into a provably correct hardware design with a program transformation called temporal staging. We illustrate this methodology with case studies including one for the BLAKE2b cryptographic hash function. Because the reference algorithm, the temporal staging transformation, and the resulting implementation are all expressed in ReWire, formal verification can proceed immediately via a published ReWire semantics. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2023\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Formalized High Level Synthesis with Applications to Cryptographic Hardware.\n \n \n \n \n\n\n \n Harrison, W. L.; Blumenfeld, I.; Bond, E.; Hathhorn, C.; Li, P.; Torrence, M.; and Ziegler, J.\n\n\n \n\n\n\n In NASA Formal Methods Symposium (NFM23), 2023. \n \n\n\n\n
\n\n\n\n \n \n \"Formalized paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison23,\n  title = {Formalized High Level Synthesis with Applications to Cryptographic Hardware},\n  author = {Harrison, William L. and Blumenfeld, Ian and Bond, Eric and Hathhorn, Chris and Li, Paul and Torrence, May and Ziegler, Jared},\n  booktitle = {NASA Formal Methods Symposium (NFM23)},\n  year = {2023},\n  abstract = {\n  Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, \nthe more optimized for performance an accelerator is, the more challenging its verification. This paper introduces a verification methodology, \\emph{model validation}, that uses a formalized high-level synthesis language (FHLS) as an intermediary between algorithm specification and hardware implementation. The foundation of our approach to model validation is a mechanized denotational semantics for the ReWire HLS language. Model validation proves the faithfulness of FHLS models to the RTL implementation and we summarize a model validation case study for a suite of pipelined Barrett multipliers.\n},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/nfm23.pdf",\n}\n\n
\n
\n\n\n
\n Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, the more optimized for performance an accelerator is, the more challenging its verification. This paper introduces a verification methodology, \\emphmodel validation, that uses a formalized high-level synthesis language (FHLS) as an intermediary between algorithm specification and hardware implementation. The foundation of our approach to model validation is a mechanized denotational semantics for the ReWire HLS language. Model validation proves the faithfulness of FHLS models to the RTL implementation and we summarize a model validation case study for a suite of pipelined Barrett multipliers. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Distributed Relation Algebra.\n \n \n \n \n\n\n \n Allwein, G.; and Harrison, W. L.\n\n\n \n\n\n\n In Bimbó, K., editor(s), Relevance Logics and other Tools for Reasoning. Essays in Honor of J. Michael Dunn, pages 1-30. College Publications, 2022.\n \n\n\n\n
\n\n\n\n \n \n \"Distributed paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{allwein2022,\nauthor = "Allwein, Gerard and Harrison, William L.",\neditor = "Bimb{\\'o}, Katalin",\ntitle = "Distributed Relation Algebra",\nbookTitle = "Relevance Logics and other Tools for Reasoning. Essays in Honor of J. Michael Dunn",\nyear = "2022",\npublisher = "College Publications",\npages = "1-30",\nisbn = "978-1-84890-395-1",\nabstract = {We define some extra relation operators in Relation Algebras and examine the relationship between Relation Algebras and Relevance Logic. We then extract binary relations from Kripke models of Relation Algebras and extend those to Distributed Relation Algebras. The term distribution refers to using a multigraph of local logics connected by the relation operators. In the context of Kripke frames for Relation Algebras, the distribution refers to a multigraph of Stone spaces each supporting a local Kripke frame. There are then distributed Kripke relations connecting the local frames. Finally, we show the relationship between the relation operators and Kan extensions and lifts from category theory.},\n        url_Paper = "https://harrisonwl.github.io/assets/papers/dist_rel_alg.pdf",\n}\n\n
\n
\n\n\n
\n We define some extra relation operators in Relation Algebras and examine the relationship between Relation Algebras and Relevance Logic. We then extract binary relations from Kripke models of Relation Algebras and extend those to Distributed Relation Algebras. The term distribution refers to using a multigraph of local logics connected by the relation operators. In the context of Kripke frames for Relation Algebras, the distribution refers to a multigraph of Stone spaces each supporting a local Kripke frame. There are then distributed Kripke relations connecting the local frames. Finally, we show the relationship between the relation operators and Kan extensions and lifts from category theory.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Mechanized Semantic Metalanguage for High Level Synthesis.\n \n \n \n \n\n\n \n Harrison, W. L.; Hathhorn, C.; and Allwein, G.\n\n\n \n\n\n\n In 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021), 2021. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison21,\n  title = {A Mechanized Semantic Metalanguage for High Level Synthesis},\n  author = {Harrison, William L. and Hathhorn, Chris and Allwein, Gerard},\n  booktitle = {23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021)},\n  year = {2021},\n  abstract = {High-level synthesis (HLS) seeks to make hardware development more like software development by adapting ideas from programming languages to hardware description and HLS from functional languages is usually motivated as a means of bringing software-like productivity to hardware development. Formalized semantics support a range of important capabilities in software languages (e.g., compositionality, comprehensibility, interoperability, formal methods, and security) that are desirable in hardware languages as well. This paper considers the formalized semantics of the Device Calculus, a typed lambda-calculus with operators for constructing Mealy machines that forms a semantic substratum suitable for high-level synthesis and we demonstrate the utility of the Device Calculus as a foundation for formal methods in functional HLS with a case study specifying the semantics of an idealized subset of the FIRRTL language. FIRRTL  (``Flexible Internal Representation for RTL'') is an open-source hardware intermediate representation targeted by the Chisel hardware construction language and the semantics we present is also a starting point for exploring formal methods and security within both the Chisel toolchain and any other high-level synthesis flows that target FIRRTL.\n},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/ppdp21.pdf",\n}\n\n
\n
\n\n\n
\n High-level synthesis (HLS) seeks to make hardware development more like software development by adapting ideas from programming languages to hardware description and HLS from functional languages is usually motivated as a means of bringing software-like productivity to hardware development. Formalized semantics support a range of important capabilities in software languages (e.g., compositionality, comprehensibility, interoperability, formal methods, and security) that are desirable in hardware languages as well. This paper considers the formalized semantics of the Device Calculus, a typed lambda-calculus with operators for constructing Mealy machines that forms a semantic substratum suitable for high-level synthesis and we demonstrate the utility of the Device Calculus as a foundation for formal methods in functional HLS with a case study specifying the semantics of an idealized subset of the FIRRTL language. FIRRTL (``Flexible Internal Representation for RTL'') is an open-source hardware intermediate representation targeted by the Chisel hardware construction language and the semantics we present is also a starting point for exploring formal methods and security within both the Chisel toolchain and any other high-level synthesis flows that target FIRRTL. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Verifiable Security Templates for Hardware.\n \n \n \n \n\n\n \n Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the Design, Automation, and Test Europe (DATE) Conference, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"Verifiable paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison20,\n  title = {Verifiable Security Templates for Hardware},\n  author = {Harrison, William L. and Allwein, Gerard},\n  booktitle = {Proceedings of the Design, Automation, and Test Europe (DATE) Conference},\n  year = {2020},\n  abstract = {High-level synthesis (HLS) research generally focuses on transferring ``software engineering virtues'' (e.g., modularity, abstraction, extensibility, etc.) to hardware development with the ultimate goal of making hardware development as agile as software development. And recent HLS research has focused on transferring ideas and techniques from high assurance software formal methods to hardware development. Just as it has introduced software engineering virtues, we believe HLS can also become a vector for adapting software formal methods to the challenge of high assurance security in hardware. This paper introduces the Device Calculus and its mechanization in the Agda proof checking system. The Device Calculus is a starting point for exploring the formal methods and security of high-level synthesis flows. We illustrate the Device Calculus with a number of examples of formally verifiable security templates---i.e., functions in the Device Calculus that express common security structures at a high-level of abstraction.\n},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/date20.pdf",\n}\n\n
\n
\n\n\n
\n High-level synthesis (HLS) research generally focuses on transferring ``software engineering virtues'' (e.g., modularity, abstraction, extensibility, etc.) to hardware development with the ultimate goal of making hardware development as agile as software development. And recent HLS research has focused on transferring ideas and techniques from high assurance software formal methods to hardware development. Just as it has introduced software engineering virtues, we believe HLS can also become a vector for adapting software formal methods to the challenge of high assurance security in hardware. This paper introduces the Device Calculus and its mechanization in the Agda proof checking system. The Device Calculus is a starting point for exploring the formal methods and security of high-level synthesis flows. We illustrate the Device Calculus with a number of examples of formally verifiable security templates—i.e., functions in the Device Calculus that express common security structures at a high-level of abstraction. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Strongly Bounded Termination with Applications to Security and Hardware Synthesis.\n \n \n \n \n\n\n \n Reynolds, T.; Chadha, R.; Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n In ACM Workshop on Type Driven Development (TyDe), 2020. \n \n\n\n\n
\n\n\n\n \n \n \"Strongly paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{reynolds20,\n  title = {Strongly Bounded Termination with Applications to Security and Hardware Synthesis},\n  author = {Reynolds, Thomas and Chadha, Rohit and Harrison, William L. and Allwein, Gerard},\n  booktitle = {ACM Workshop on Type Driven Development (TyDe)},\n  year = {2020},\n  abstract = {Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly- bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed λ-calculus called the bounded-time lambda calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well.},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/tyde20.pdf",\n  }\n\n
\n
\n\n\n
\n Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly- bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed λ-calculus called the bounded-time lambda calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Information Flow and Homotopy Theory.\n \n \n \n \n\n\n \n Allwein, G.; and Harrison, W. L.\n\n\n \n\n\n\n Journal of Logical and Algebraic Methods in Programming (under submission). 2019.\n \n\n\n\n
\n\n\n\n \n \n \"Information paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{allwein19,\n  title = {Information Flow and Homotopy Theory},\n  author = {Allwein, Gerard and Harrison, William L.},\n  journal = {Journal of Logical and Algebraic Methods in Programming (under submission)},\n  year = {2019},\n  numpages = {38},                \n  abstract = {Simulation and bisimulation are used in many areas of security in Computing Science, however the methods used do not come with a supporting logic giving the regularities of information flow. We have developed Distributed Logic to represent regularities governing information flow between localities of a distributed system, each locality can be outfitted with its own notion of state and language. The flows, either internal to a locality or between localities, follow a connection structure specified by a graph in the logic and semantically by relations in a category. We use some basic homotopy notions for use in distributed systems by using the notions as a template for properties of (bi)simulations useful for security and other properties of distributed systems. The logic can express formulas whose validity is unwritten by the (bi)simulations. This presents new ways of formalizing and proving properties of distributed systems.},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/dist_hom_theory.pdf",\n}\n\n\n
\n
\n\n\n
\n Simulation and bisimulation are used in many areas of security in Computing Science, however the methods used do not come with a supporting logic giving the regularities of information flow. We have developed Distributed Logic to represent regularities governing information flow between localities of a distributed system, each locality can be outfitted with its own notion of state and language. The flows, either internal to a locality or between localities, follow a connection structure specified by a graph in the logic and semantically by relations in a category. We use some basic homotopy notions for use in distributed systems by using the notions as a template for properties of (bi)simulations useful for security and other properties of distributed systems. The logic can express formulas whose validity is unwritten by the (bi)simulations. This presents new ways of formalizing and proving properties of distributed systems.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware.\n \n \n \n \n\n\n \n Reynolds, T. N.; Procter, A.; Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n ACM Transactions on Embedded Computing Systems, 18(1): 6:1–6:26. January 2019.\n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{reynolds19,\n author = {Reynolds, Thomas N. and Procter, Adam and Harrison, William L. and Allwein, Gerard},\n title = {The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware},\n journal = {ACM Transactions on Embedded Computing Systems},\n issue_date = {February 2019},\n volume = {18},\n number = {1},\n month = jan,\n year = {2019},\n issn = {1539-9087},\n pages = {6:1--6:26},\n articleno = {6},\n numpages = {26},\n keywords = {High-level synthesis, hardware verification, security},\n\tabstract = {\n\t\tConstructing high assurance, secure hardware remains a challenge, because to do so relies on both a verifiable means of hardware description and implementation. \n\tHowever, production hardware description languages (HDL) lack the formal underpinnings required by formal methods in security.\n\tStill, there is no such thing as high assurance systems without high assurance hardware.\n\tWe present a core calculus of secure hardware description with its formal semantics, security type system and mechanization in Coq. \n\tThis calculus is the core of the functional HDL, ReWire, shown in previous work to have useful applications in reconfigurable computing.\n\tThis work supports a full-fledged, formal methodology for producing high assurance hardware.\n},\n        url_Paper = "https://harrisonwl.github.io/assets/papers/tecs18.pdf",\n} \n\n \n\n
\n
\n\n\n
\n Constructing high assurance, secure hardware remains a challenge, because to do so relies on both a verifiable means of hardware description and implementation. However, production hardware description languages (HDL) lack the formal underpinnings required by formal methods in security. Still, there is no such thing as high assurance systems without high assurance hardware. We present a core calculus of secure hardware description with its formal semantics, security type system and mechanization in Coq. This calculus is the core of the functional HDL, ReWire, shown in previous work to have useful applications in reconfigurable computing. This work supports a full-fledged, formal methodology for producing high assurance hardware. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Language Abstractions for Hardware-based Control-Flow Integrity Monitoring.\n \n \n \n \n\n\n \n Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 2018 International Conference on Reconfigurable Computing and FPGAs, pages 1-6, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"Language paper\n  \n \n \n \"Language code\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison18b,\n  title = {Language Abstractions for Hardware-based Control-Flow Integrity Monitoring},\n  author = {Harrison, William L. and Allwein, Gerard},\n  booktitle = {Proceedings of the 2018 International Conference on Reconfigurable Computing and FPGAs},\n  year = {2018},\n  pages = {1-6},\n  abstract = {Control-Flow Integrity (CFI) is a software protection mechanism that \ndetects a class of code reuse attacks by identifying anomalous control-flows within an executing program. Hardware-based CFI has the promise of the security benefits of CFI without the performance overhead and complexity of software-based CFI: generally speaking, hardware-based monitors are more difficult to bypass, offer lower performance overheads than software-based monitors, and, furthermore, hardware-based CFI can be performed without the necessity of altering application binaries or instrumenting language compilers. Although hardware-based CFI is an active area of research and there is a growing literature describing CFI strategies at a high-level, there is, to the authors' best knowledge, no work on languages specially tailored to the specification and implementation of CFI monitors. This article presents a proof-of-concept domain-specific language with built-in abstractions for expressing control-flow constraints along with a compiler that targets the functional hardware description language ReWire. While the case study is small, it indicates, we argue, an approach to rapid-prototyping hardware-based monitors enforcing CFI that is quick, flexible, and extensible as well as being amenable to formal verification.\n},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/reconfig18.pdf",\n  url_Code  = "https://harrisonwl.github.io/assets/code/ReConFig18codebase.tar.gz",\n}\n\n
\n
\n\n\n
\n Control-Flow Integrity (CFI) is a software protection mechanism that detects a class of code reuse attacks by identifying anomalous control-flows within an executing program. Hardware-based CFI has the promise of the security benefits of CFI without the performance overhead and complexity of software-based CFI: generally speaking, hardware-based monitors are more difficult to bypass, offer lower performance overheads than software-based monitors, and, furthermore, hardware-based CFI can be performed without the necessity of altering application binaries or instrumenting language compilers. Although hardware-based CFI is an active area of research and there is a growing literature describing CFI strategies at a high-level, there is, to the authors' best knowledge, no work on languages specially tailored to the specification and implementation of CFI monitors. This article presents a proof-of-concept domain-specific language with built-in abstractions for expressing control-flow constraints along with a compiler that targets the functional hardware description language ReWire. While the case study is small, it indicates, we argue, an approach to rapid-prototyping hardware-based monitors enforcing CFI that is quick, flexible, and extensible as well as being amenable to formal verification. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Semantics-directed Prototyping of Hardware Runtime Monitors.\n \n \n \n \n\n\n \n Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 29th International Symposium on Rapid System Prototyping (RSP), October 2018. \n \n\n\n\n
\n\n\n\n \n \n \"Semantics-directed paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison18a,\n  title = {Semantics-directed Prototyping of Hardware Runtime Monitors},\n  author = {Harrison, William L. and Allwein, Gerard},\n  booktitle = {Proceedings of the 29th International Symposium on Rapid System Prototyping (RSP)},\n  month = Oct,\n  year = {2018},\n  abstract = {Building memory protection mechanisms into embedded hardware is attractive because it has the potential to neutralize a host of software-based attacks with relatively small performance overhead. A hardware monitor, being at the lowest level of the system stack, is more difficult to bypass than a software monitor and hardware-based protections are also potentially more fine-grained than is possible in software: an individual instruction executing on a processor may entail multiple memory accesses, all of which may be tracked in hardware. Finally, hardware-based protection can be performed without the necessity of altering application binaries. This article presents a proof-of-concept codesign of a small embedded processor with a hardware monitor protecting against ROP-style code reuse attacks. While the case study is small, it indicates, we argue, an approach to rapid-prototyping runtime monitors in hardware that is quick, flexible, and extensible as well as being amenable to formal verification.},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/rsp18.pdf",\n}\n\n\n
\n
\n\n\n
\n Building memory protection mechanisms into embedded hardware is attractive because it has the potential to neutralize a host of software-based attacks with relatively small performance overhead. A hardware monitor, being at the lowest level of the system stack, is more difficult to bypass than a software monitor and hardware-based protections are also potentially more fine-grained than is possible in software: an individual instruction executing on a processor may entail multiple memory accesses, all of which may be tracked in hardware. Finally, hardware-based protection can be performed without the necessity of altering application binaries. This article presents a proof-of-concept codesign of a small embedded processor with a hardware monitor protecting against ROP-style code reuse attacks. While the case study is small, it indicates, we argue, an approach to rapid-prototyping runtime monitors in hardware that is quick, flexible, and extensible as well as being amenable to formal verification.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Core Calculus for Secure Hardware: Its Formal Semantics and Proof System.\n \n \n \n \n\n\n \n Reynolds, T. N.; Procter, A.; Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE17), 2017. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{reynolds17,\n  title = {A Core Calculus for Secure Hardware: Its Formal Semantics and Proof System},\n  author = {Reynolds, Thomas N. and Procter, Adam and Harrison, William L. and Allwein, Gerard},\n  booktitle = {Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE17)},\n  year = {2017},\n  abstract = {Constructing high assurance, secure hardware remains a challenge, because to do so relies on both a verifiable means of hardware description and implementation. However, production hardware description languages (HDL) lack the formal underpinnings required by formal methods in security. Still, there is no such thing as high assurance systems without high assurance hardware. We present a core calculus of secure hardware description with its formal semantics, security type system and mechanization in Coq. This calculus is the core of the functional HDL, ReWire, shown in previous work to have useful applications in reconfigurable computing. This work supports a full-fledged, formal methodology for producing high assurance hardware.},\n  url_Paper = "https://harrisonwl.github.io/assets/papers/memocode17.pdf",\n}\n                  \n
\n
\n\n\n
\n Constructing high assurance, secure hardware remains a challenge, because to do so relies on both a verifiable means of hardware description and implementation. However, production hardware description languages (HDL) lack the formal underpinnings required by formal methods in security. Still, there is no such thing as high assurance systems without high assurance hardware. We present a core calculus of secure hardware description with its formal semantics, security type system and mechanization in Coq. This calculus is the core of the functional HDL, ReWire, shown in previous work to have useful applications in reconfigurable computing. This work supports a full-fledged, formal methodology for producing high assurance hardware.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Distributed Relation Logic.\n \n \n \n \n\n\n \n Allwein, G.; Harrison, W. L.; and Reynolds, T.\n\n\n \n\n\n\n Logic and Logical Philosophy, 26(1): 19-61. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Distributed paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@article{allwein17,\n\tauthor = {Gerard Allwein and William L. Harrison and Thomas Reynolds},\n\ttitle = {Distributed Relation Logic},\n\tjournal = {Logic and Logical Philosophy},\n\tvolume = {26},\n\tnumber = {1},\n        pages = {19-61},          \n\tyear = {2017},\n\tkeywords = {relation algebra; multisorted algebra; distributed logic; Kripke frames; Kripke models},\n\tabstract = {We extend the relational algebra of Chin and Tarski so that it is multisorted or, as we prefer, typed. Each type supports a local Boolean algebra outfitted with a converse operator. From Lyndon, we know that relation algebras cannot be represented as proper relation algebras where a proper relation algebra has binary relations as elements and the algebra is singly-typed. Here, the intensional conjunction, which was to represent relational composition in Chin and Tarski, spans three different local algebras, thus the term distributed in the title. Since we do not rely on proper relation algebras, we are free to re-express the algebras as typed. In doing so, we allow many different intensional conjunction operators.We construct a typed logic over these algebras, also known as heterogeneous algebras of Birkhoff and Lipson. The logic can be seen as a form of relevance logic with a classical negation connective where the Routley-Meyer star operator is reified as a converse connective in the logic. Relevance logic itself is not typed but our work shows how it can be made so. Some of the properties of classical relevance logic are weakened from Routley-Meyer’s version which is too strong for a logic over relation algebras.},\n\tissn = {2300-9802},\n   url_Paper = "https://harrisonwl.github.io/assets/papers/llp17.pdf",\n\n}\n                  \n
\n
\n\n\n
\n We extend the relational algebra of Chin and Tarski so that it is multisorted or, as we prefer, typed. Each type supports a local Boolean algebra outfitted with a converse operator. From Lyndon, we know that relation algebras cannot be represented as proper relation algebras where a proper relation algebra has binary relations as elements and the algebra is singly-typed. Here, the intensional conjunction, which was to represent relational composition in Chin and Tarski, spans three different local algebras, thus the term distributed in the title. Since we do not rely on proper relation algebras, we are free to re-express the algebras as typed. In doing so, we allow many different intensional conjunction operators.We construct a typed logic over these algebras, also known as heterogeneous algebras of Birkhoff and Lipson. The logic can be seen as a form of relevance logic with a classical negation connective where the Routley-Meyer star operator is reified as a converse connective in the logic. Relevance logic itself is not typed but our work shows how it can be made so. Some of the properties of classical relevance logic are weakened from Routley-Meyer’s version which is too strong for a logic over relation algebras.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Principled Approach to Secure Multi-Core Processor Design with ReWire.\n \n \n \n \n\n\n \n Procter, A.; Harrison, W. L.; Graves, I.; Becchi, M.; and Allwein, G.\n\n\n \n\n\n\n ACM Transactions on Embedded Computing Systems, 16(2): 33:1–33:25. January 2017.\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{procter16,                  \n author = {Procter, Adam and Harrison, William L. and Graves, Ian and Becchi, Michela and Allwein, Gerard},\n title = {A Principled Approach to Secure Multi-Core Processor Design with ReWire},\n\tjournal = {ACM Transactions on Embedded Computing Systems},\n issue_date = {April 2017},\n volume = {16},\n number = {2},\n month = jan,\n year = {2017},\n issn = {1539-9087},\n pages = {33:1--33:25},\n articleno = {33},\n numpages = {25},\n\tabstract = {There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper advocates a {\\em semantics-directed} approach to bridge this conceptual gap. We present a case study in the design of secure processors, which are formally derived via principled techniques grounded in functional programming and equational reasoning. The case study comprises the development of secure single- and dual-core variants of a single processor, both based on a common semantic specification of the ISA. We demonstrate via formal equational reasoning that the dual-core processor respects a ``no-write-down'' information flow policy. The semantics-directed approach enables a modular and extensible style of system design and verification. The secure processors require only a very small amount of additional code to specify and implement, and their security verification arguments are concise and readable. Our approach rests critically on ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs. This case study demonstrates both ReWire's expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.\n},\n        url_Paper = "https://harrisonwl.github.io/assets/papers/tecs16.pdf",\n}\n\n\n\n
\n
\n\n\n
\n There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper advocates a \\em semantics-directed approach to bridge this conceptual gap. We present a case study in the design of secure processors, which are formally derived via principled techniques grounded in functional programming and equational reasoning. The case study comprises the development of secure single- and dual-core variants of a single processor, both based on a common semantic specification of the ISA. We demonstrate via formal equational reasoning that the dual-core processor respects a ``no-write-down'' information flow policy. The semantics-directed approach enables a modular and extensible style of system design and verification. The secure processors require only a very small amount of additional code to specify and implement, and their security verification arguments are concise and readable. Our approach rests critically on ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs. This case study demonstrates both ReWire's expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Model-driven Design & Synthesis of the SHA-256 Cryptographic Hash Function in ReWire.\n \n \n \n \n\n\n \n Harrison, W. L.; Procter, A.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 27th International Symposium on Rapid System Prototyping (RSP), pages 1-7, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"Model-driven paper\n  \n \n \n \"Model-driven slides\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison16a,\n   title = {Model-driven Design \\& Synthesis of the SHA-256 Cryptographic Hash Function in ReWire},\n   author = {Harrison, William L. and Procter, Adam and Allwein, Gerard},\n   booktitle = {Proceedings of the 27th International Symposium on Rapid System Prototyping (RSP)},\n   year = {2016},\n   pages = {1-7},\n   abstract = {There are many algorithms whose implementations can benefit both from hardware acceleration and formal verification and we would like to develop high assurance implementations as rapidly as possible. Critical computing infrastructure like cryptographic algorithms are prime candidates both for such acceleration and for formal verification. We show how to derive a verifiable, hardware-accelerated implementation of the SHA-256 cryptographic hash in the ReWire functional hardware description language in which the partitioning of the implementation between hardware and software is reflected in the type system itself.\n},\n   url_Paper = "https://harrisonwl.github.io/assets/papers/rsp16.pdf",\n   url_Slides = "https://harrisonwl.github.io/assets/papers/slides-rsp16.pdf",\n  }\n                  \n
\n
\n\n\n
\n There are many algorithms whose implementations can benefit both from hardware acceleration and formal verification and we would like to develop high assurance implementations as rapidly as possible. Critical computing infrastructure like cryptographic algorithms are prime candidates both for such acceleration and for formal verification. We show how to derive a verifiable, hardware-accelerated implementation of the SHA-256 cryptographic hash in the ReWire functional hardware description language in which the partitioning of the implementation between hardware and software is reflected in the type system itself. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Distributed Modal Logic.\n \n \n \n \n\n\n \n Allwein, G.; and Harrison, W. L.\n\n\n \n\n\n\n In Bimbó, K., editor(s), J. Michael Dunn on Information Based Logics, pages 331–362. Springer International Publishing, 2016.\n \n\n\n\n
\n\n\n\n \n \n \"DistributedPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{allwein2016a,\nauthor = "Allwein, Gerard and Harrison, William L.",\neditor = "Bimb{\\'o}, Katalin",\ntitle = "Distributed Modal Logic",\nbookTitle = "J. Michael Dunn on Information Based Logics",\nyear = "2016",\npublisher = "Springer International Publishing",\npages = "331--362",\nisbn = "978-3-319-29300-4",\nurl="http://dx.doi.org/10.1007/978-3-319-29300-4_16"\n}\n                  \n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Programming Model for Reconfigurable Computing Based in Functional Concurrency.\n \n \n \n \n\n\n \n Harrison, W. L.; Procter, A.; Graves, I.; Becchi, M.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC 2016), 2016. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n \n \"A slides\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison16,\n   title = {A Programming Model for Reconfigurable Computing Based in Functional Concurrency},\n   author = {Harrison, William L. and Procter, Adam and Graves, Ian and Becchi, Michela and Allwein, Gerard},\n   booktitle = {Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC 2016)},\n   year = {2016},\n   pages = {},\n   abstract = {FPGA programmability remains a concern with respect to the broad adoption of the technology. One reason for this is simple: FPGA applications are frequently implementations of concurrent algorithms that could be most directly rendered in concurrent languages, but there is little or no first-class support for concurrent applications in conventional hardware description languages. It stands to reason that FPGA programmability would be enhanced in a hardware description language with first-class concurrency. The starting point for this paper is a functional hardware description language with built-in support for concurrency called ReWire. Because it is a concurrent functional language, ReWire supports the elegant expression of common concurrency paradigms; we illustrate this with several case studies. },                  \n   url_Paper = "https://harrisonwl.github.io/assets/papers/recosoc16.pdf",\n   url_Slides = "https://harrisonwl.github.io/assets/papers/slides-recosoc16.pdf",\n  }\n\n  \n
\n
\n\n\n
\n FPGA programmability remains a concern with respect to the broad adoption of the technology. One reason for this is simple: FPGA applications are frequently implementations of concurrent algorithms that could be most directly rendered in concurrent languages, but there is little or no first-class support for concurrent applications in conventional hardware description languages. It stands to reason that FPGA programmability would be enhanced in a hardware description language with first-class concurrency. The starting point for this paper is a functional hardware description language with built-in support for concurrency called ReWire. Because it is a concurrent functional language, ReWire supports the elegant expression of common concurrency paradigms; we illustrate this with several case studies. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Cheap (But Functional) Threads.\n \n \n \n \n\n\n \n Harrison, W. L.; and Procter, A.\n\n\n \n\n\n\n Higher Order and Symbolic Computation (accepted for publication). 2015.\n Draft version\n\n\n\n
\n\n\n\n \n \n \"Cheap paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@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
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Provably Correct Development of reconfigurable hardware designs via equational reasoning.\n \n \n \n \n\n\n \n Graves, I.; Procter, A. M.; Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 2015 International Conference on Field-Programmable Technology (FPT '15), pages 160-171, 2015. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"Provably paper\n  \n \n \n \"Provably slides\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{graves15a,\n  author = {Graves, Ian and Procter, Adam M. and Harrison, William L. and Allwein, Gerard},\n  booktitle = {Proceedings of the 2015 International Conference on\nField-Programmable Technology (FPT '15)},\n  isbn = {978-1-4673-9091-0},\n  pages = {160-171},\n  publisher = {IEEE},\n  title = {Provably Correct Development of reconfigurable hardware designs via equational reasoning.},\n  year = 2015,\n  url_Paper = "https://harrisonwl.github.io/assets/papers/fpt15.pdf",\n  url_Slides = "https://harrisonwl.github.io/assets/papers/slides-fpt15.pdf",\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Semantics Driven Hardware Design, Implementation, and Verification with ReWire.\n \n \n \n \n\n\n \n Procter, A.; Harrison, W. L.; Graves, I.; Becchi, M.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM, of LCTES'15, pages 13:1–13:10, 2015. \n \n\n\n\n
\n\n\n\n \n \n \"Semantics paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{procter15,\n author = {Procter, Adam and Harrison, William L. and Graves, Ian and Becchi, Michela and Allwein, Gerard},\n title = {Semantics Driven Hardware Design, Implementation, and Verification with ReWire},\n booktitle = {Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM},\n series = {LCTES'15},\n year = {2015},\n isbn = {978-1-4503-3257-6},\n location = {Portland, OR, USA},\n pages = {13:1--13:10},\n articleno = {13},\n numpages = {10},\n abstract = "There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper presents ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs, and a compiler for that language that translates high-level, semantics-driven designs directly into working hardware. ReWire's design and implementation are presented, along with a case study in the design of a secure multicore processor, demonstrating both ReWire's expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.",                 \n url_Paper = {https://harrisonwl.github.io/assets/papers/lctes15.pdf},\n} \n\n                  \n\n
\n
\n\n\n
\n There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper presents ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs, and a compiler for that language that translates high-level, semantics-driven designs directly into working hardware. ReWire's design and implementation are presented, along with a case study in the design of a secure multicore processor, demonstrating both ReWire's expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Hardware Synthesis from Functional Embedded Domain-Specific Languages: A Case Study in Regular Expression Compilation.\n \n \n \n \n\n\n \n Graves, I.; Procter, A.; Harrison, W. L.; Becchi, M.; and Allwein, G.\n\n\n \n\n\n\n In Sano, K.; Soudris, D.; Huebner, M.; and Diniz, P. C., editor(s), Applied Reconfigurable Computing, volume 9040, of Lecture Notes in Computer Science, pages 41-52. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"Hardware paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{graves15,\nyear={2015},\nbooktitle={Applied Reconfigurable Computing},\nvolume={9040},\nseries={Lecture Notes in Computer Science},\neditor={Sano, Kentaro and Soudris, Dimitrios and Huebner, Michael and Diniz, Pedro C.},\ntitle={Hardware Synthesis from Functional Embedded Domain-Specific Languages: A Case Study in Regular Expression Compilation},\nauthor={Graves, Ian and Procter, Adam and Harrison, William L. and Becchi, Michela and Allwein, Gerard},\npages={41-52},\nabstract = "Although FPGAs have the potential to bring software-like flexibility and agility to the hardware world, designing for FPGAs remains a difficult task divorced from standard software engineering norms. A better programming flow would go far towards realizing the potential of widely deployed, programmable hardware. We propose a general methodology based on domain specific languages embedded in the functional language Haskell to bridge the gap between high level abstractions that support programmer productivity and the need for high performance in FPGA circuit implementations. We illustrate this methodology with a framework for regular expression to hardware compilers, written in Haskell, that supports high programmer productivity while producing circuits whose performance matches and, indeed, exceeds that of a state of the art, hand-optimized VHDL-based tool. For example, after applying a  novel optimization pass, throughput increased an average of 28.3 percent over the state of the art tool for one set of benchmarks.",\n url_Paper = "https://harrisonwl.github.io/assets/papers/arc15.pdf",\n}\n\n\n
\n
\n\n\n
\n Although FPGAs have the potential to bring software-like flexibility and agility to the hardware world, designing for FPGAs remains a difficult task divorced from standard software engineering norms. A better programming flow would go far towards realizing the potential of widely deployed, programmable hardware. We propose a general methodology based on domain specific languages embedded in the functional language Haskell to bridge the gap between high level abstractions that support programmer productivity and the need for high performance in FPGA circuit implementations. We illustrate this methodology with a framework for regular expression to hardware compilers, written in Haskell, that supports high programmer productivity while producing circuits whose performance matches and, indeed, exceeds that of a state of the art, hand-optimized VHDL-based tool. For example, after applying a novel optimization pass, throughput increased an average of 28.3 percent over the state of the art tool for one set of benchmarks.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Distributed Logics.\n \n \n \n \n\n\n \n Allwein, G.; and Harrison, W. L.\n\n\n \n\n\n\n Technical Report NRL/MR/5540-14-9565, US Naval Research Laboratory, 2014.\n \n\n\n\n
\n\n\n\n \n \n \"Distributed paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@TechReport{allwein14,\n  author = \t {Gerard Allwein and William L. Harrison},\n  title = \t {{Distributed Logics}},\n  institution =  {US Naval Research Laboratory},\n  number =       "NRL/MR/5540-14-9565",\n  year = \t 2014,\n  htr =          "yes",\n  url_Paper =    "https://harrisonwl.github.io/assets/papers/dist-logics-tech-report.pdf",\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Semantics-directed Machine Architecture in ReWire.\n \n \n \n \n\n\n \n Procter, A.; Harrison, W. L.; Graves, I.; Becchi, M.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 2013 International Conference on Field Programmable Technology, pages 446-449, Dec 2013. \n \n\n\n\n
\n\n\n\n \n \n \"Semantics-directed paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{icfpt13,\n   title = "Semantics-directed Machine Architecture in ReWire",\n   booktitle = "Proceedings of the 2013 International Conference on Field Programmable Technology",\n   author = "Adam Procter and William L. Harrison and Ian Graves and Michela Becchi and Gerard Allwein",\n   year = 2013,\nmonth={Dec}, \npages={446-449}, \nabstract={The functional programming community has developed a number of powerful abstractions for dealing with diverse programming models in a modular way. Beginning with a core of pure, side effect free computation, modular monadic semantics (MMS) allows designers to construct domain-specific languages by adding layers of semantic features, such as mutable state and I/O, in an a' la carte fashion. In the realm of interpreter and compiler construction, the benefits of this approach are manifold and well explored. This paper advocates bringing the tools of MMS to bear on hardware design and verification. In particular, we shall discuss a prototype compiler called ReWire which translates high-level MMS hardware specifications into working circuits on FPGAs. This enables designers to tackle the complexity of hardware design in a modular way, without compromising efficiency.}, \nkeywords={electronic engineering computing;field programmable gate arrays;formal verification;functional programming;program compilers;FPGA;MMS;ReWire;compiler construction;diverse programming models;domain-specific languages;functional programming;hardware design;modular monadic semantics;semantics-directed machine architecture;verification;Field programmable gate arrays;Hardware;Microcontrollers;Ports (Computers);Random access memory;Registers;Semantics}, \n    url_Paper = "https://harrisonwl.github.io/assets/papers/icfpt13.pdf",\n}\n\n
\n
\n\n\n
\n The functional programming community has developed a number of powerful abstractions for dealing with diverse programming models in a modular way. Beginning with a core of pure, side effect free computation, modular monadic semantics (MMS) allows designers to construct domain-specific languages by adding layers of semantic features, such as mutable state and I/O, in an a' la carte fashion. In the realm of interpreter and compiler construction, the benefits of this approach are manifold and well explored. This paper advocates bringing the tools of MMS to bear on hardware design and verification. In particular, we shall discuss a prototype compiler called ReWire which translates high-level MMS hardware specifications into working circuits on FPGAs. This enables designers to tackle the complexity of hardware design in a modular way, without compromising efficiency.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Quantitative Analysis of Error Injection Covert Channels.\n \n \n \n \n\n\n \n Harrison, R.; and Harrison, W. L.\n\n\n \n\n\n\n In Proceedings of the International Workshop on Quantitative Aspects in Security Assurance (QASA13), 2013. \n \n\n\n\n
\n\n\n\n \n \n \"Quantitative paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{qasa13,\n   title = "Quantitative Analysis of Error Injection Covert Channels",\n   booktitle = "Proceedings of the International Workshop on Quantitative Aspects in Security Assurance (QASA13)",\n   author = "Robert Harrison and William L. Harrison",\n   year = 2013,\n   abstract = "Covert channels are mechanisms for communication where a legitimate channel carries a hidden message, and where the hidden message is conveyed using legal operations of the legitimate channel. Quantitative modeling of the response of the covert channel to noise results in an enhanced understanding of the channel and delimits the range of conditions under which a covert channel can operate effectively. The analysis of two covert channels using the confusion matrix and noise models shows that the techniques presented in this paper are widely applicable to covert information flows in noisy channels.",               \n    url_Paper = "https://harrisonwl.github.io/assets/papers/interchannel.pdf",\n}\n\n
\n
\n\n\n
\n Covert channels are mechanisms for communication where a legitimate channel carries a hidden message, and where the hidden message is conveyed using legal operations of the legitimate channel. Quantitative modeling of the response of the covert channel to noise results in an enhanced understanding of the channel and delimits the range of conditions under which a covert channel can operate effectively. The analysis of two covert channels using the confusion matrix and noise models shows that the techniques presented in this paper are widely applicable to covert information flows in noisy channels.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Simulation logic.\n \n \n \n \n\n\n \n Allwein, G.; Harrison, W.; and Andrews, D.\n\n\n \n\n\n\n Logic and Logical Philosophy, 23(3): 277–299. Sep. 2013.\n \n\n\n\n
\n\n\n\n \n \n \"Simulation paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@article{LLP13,\n\tauthor = {Gerard Allwein and William Harrison and David Andrews},\n\ttitle = {Simulation logic},\n\tjournal = {Logic and Logical Philosophy},\n\tvolume = {23},\n\tnumber = {3},\n\tyear = {2013},\n        month={Sep.},\n        pages={277–299},\n\tkeywords = {modal logic; simulations; Hilbert systems; Kripke; modal algebras},\n\tabstract = {Simulation relations have been discovered in many areas: Computer Science, philosophical and modal logic, and set theory. However, the simulation condition is strictly a first-order logic statement. We extend modal logic with modalities and axioms, the latter's modeling conditions are the simulation conditions. The modalities are normal, i.e., commute with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The simulations are considered arrows in a category where the objects are descriptive, general frames. One can augment the simulation modalities by axioms for requiring the underlying modeling simulations to be bisimulations or to be p-morphisms. The modal systems presented are multi-sorted and both sound and complete with respect to their algebraic and Kripke semantics.},\n   url_Paper = "https://harrisonwl.github.io/assets/papers/llp2014.pdf",\n}\n\n\n
\n
\n\n\n
\n Simulation relations have been discovered in many areas: Computer Science, philosophical and modal logic, and set theory. However, the simulation condition is strictly a first-order logic statement. We extend modal logic with modalities and axioms, the latter's modeling conditions are the simulation conditions. The modalities are normal, i.e., commute with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The simulations are considered arrows in a category where the objects are descriptive, general frames. One can augment the simulation modalities by axioms for requiring the underlying modeling simulations to be bisimulations or to be p-morphisms. The modal systems presented are multi-sorted and both sound and complete with respect to their algebraic and Kripke semantics.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n The Confinement Problem in the Presence of Faults.\n \n \n \n \n\n\n \n William L. Harrison, A. P.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 2012 International Conference on Formal Engineering Methods, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ICFEM12,\n   title = "The Confinement Problem in the Presence of Faults",\n   booktitle = "Proceedings of the 2012 International Conference on Formal Engineering Methods",\n   author = "William L. Harrison, Adam Procter and Gerard Allwein",\n   year = 2012,\n   url_Paper = "https://harrisonwl.github.io/assets/papers/icfem12.pdf",\n  abstract = "In this paper, we establish a semantic foundation for the safe\nexecution of untrusted code. Our approach extends Moggi's computational $\\lambda$-calculus in two dimensions with operations for asynchronous concurrency, shared state and software faults and with an effect type system $\\grave{a}$ la Wadler providing fine-grained control of effects. An equational system for fault isolation is exhibited and its soundness demonstrated with a semantics based on monad transformers. Our formalization of the equational system in the Coq theorem prover is discussed. We argue that the approach may be generalized to capture other safety properties, including information flow security.",\n   }                  \n                  \n
\n
\n\n\n
\n In this paper, we establish a semantic foundation for the safe execution of untrusted code. Our approach extends Moggi's computational $λ$-calculus in two dimensions with operations for asynchronous concurrency, shared state and software faults and with an effect type system $à$ la Wadler providing fine-grained control of effects. An equational system for fault isolation is exhibited and its soundness demonstrated with a semantics based on monad transformers. Our formalization of the equational system in the Coq theorem prover is discussed. We argue that the approach may be generalized to capture other safety properties, including information flow security.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications.\n \n \n \n \n\n\n \n Chris Hathhorn, M. B.; and Procter, A.\n\n\n \n\n\n\n In Proceedings of the 2012 Systems Software Verification Conference, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"Formal paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{SSV12,\n   title = "Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications",\n   booktitle = "Proceedings of the 2012 Systems Software Verification Conference",\n   author = "Chris Hathhorn, Michela Becchi, William L. Harrison and Adam Procter",\n   year = 2012,\n   url_Paper = "https://harrisonwl.github.io/assets/papers/ssv12.pdf",\n  abstract = "We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosiu's K Framework semantics) with the core features of CUDA-C. The hybrid CPU/GPU computation model of CUDA-C presents challenges not just for programmers, but also for practitioners of formal methods. Our formal semantics helps expose and clarify these issues. We demonstrate the usefulness of our semantics by generating a tool from it\ncapable of detecting some race conditions and deadlocks in CUDA-C programs. We discuss limitations of our model and argue that its extensibility can easily\nenable a wider range of verification tasks.",\n   }                  \n                  \n
\n
\n\n\n
\n We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosiu's K Framework semantics) with the core features of CUDA-C. The hybrid CPU/GPU computation model of CUDA-C presents challenges not just for programmers, but also for practitioners of formal methods. Our formal semantics helps expose and clarify these issues. We demonstrate the usefulness of our semantics by generating a tool from it capable of detecting some race conditions and deadlocks in CUDA-C programs. We discuss limitations of our model and argue that its extensibility can easily enable a wider range of verification tasks.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Simulation Logic.\n \n \n \n \n\n\n \n Gerard Allwein, W. L. H.; and Andrews, D.\n\n\n \n\n\n\n In Proceedings of the 2012 Conference on Non-Classical Logics, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"Simulation paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{NCL12,\n   title = "Simulation Logic",\n   booktitle = "Proceedings of the 2012 Conference on Non-Classical Logics",\n   author = "Gerard Allwein, William L. Harrison and David Andrews",\n   year = 2012,\n   url_Paper = "https://harrisonwl.github.io/assets/papers/ncl12.pdf",\n  abstract = "Simulation relations have been discovered in many areas: Computer Science, philosophical and modal logic, and set theory. However, the simulation condition is strictly a first-order logic statement. We extend modal logic with modalities and axioms, the latter's modeling conditions are the simulation conditions. The modalities are normal, i.e., commute with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The simulations are considered arrows in a category where the objects are descriptive, general frames. One can augment the simulation modalities by axioms for requiring the underlying modeling simulations to be bisimulations or to be p-morphisms. The modal systems presented are multi-sorted and both sound and complete with respect to their algebraic and Kripke semantics.",\n   }                  \n                  \n
\n
\n\n\n
\n Simulation relations have been discovered in many areas: Computer Science, philosophical and modal logic, and set theory. However, the simulation condition is strictly a first-order logic statement. We extend modal logic with modalities and axioms, the latter's modeling conditions are the simulation conditions. The modalities are normal, i.e., commute with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The simulations are considered arrows in a category where the objects are descriptive, general frames. One can augment the simulation modalities by axioms for requiring the underlying modeling simulations to be bisimulations or to be p-morphisms. The modal systems presented are multi-sorted and both sound and complete with respect to their algebraic and Kripke semantics.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Design of a Practical Proof Checker for a Lazy Functional Language.\n \n \n \n \n\n\n \n Adam Procter, W. L. H.; and Stump, A.\n\n\n \n\n\n\n In Proceedings of the 2012 Trends in Functional Programming Conference, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{TFP12,\n   title = "The Design of a Practical Proof Checker for a Lazy Functional Language",\n   booktitle = "Proceedings of the 2012 Trends in Functional Programming Conference",\n   author = "Adam Procter, William L. Harrison and Aaron Stump",\n   year = 2012,\n   url_Paper = "https://harrisonwl.github.io/assets/papers/tfp12.pdf",\n  abstract = "Pure, lazy functional languages like Haskell provide a sound basis for formal reasoning about programs in an equational style. In\npractice, however, equational reasoning is underutilized. We suggest that part\nof the reason for this is the lack of accessible tools for developing\nmachine-checked equational reasoning proofs. This paper outlines the design of\nMProver, a system which fills just that niche. MProver features first-class\nsupport for reasoning about potentially undefined computations (particularly\nimportant in a lazy setting), and an extended notion of Haskell-like type\nclasses, enabling a highly modular style of program verification that closely\nfollows familiar functional programming idioms.",\n   }                  \n                  \n
\n
\n\n\n
\n Pure, lazy functional languages like Haskell provide a sound basis for formal reasoning about programs in an equational style. In practice, however, equational reasoning is underutilized. We suggest that part of the reason for this is the lack of accessible tools for developing machine-checked equational reasoning proofs. This paper outlines the design of MProver, a system which fills just that niche. MProver features first-class support for reasoning about potentially undefined computations (particularly important in a lazy setting), and an extended notion of Haskell-like type classes, enabling a highly modular style of program verification that closely follows familiar functional programming idioms.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Channel Theoretic Account of Separation Security.\n \n \n \n \n\n\n \n Allwein, G.; and Harrison, W. L.\n\n\n \n\n\n\n In Proceedings of the 2011 International Conference on Engineering Reconfigurable Systems and Algorithms (ERSA11), 2011. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ERSA2011a,\n   title = "A Channel Theoretic Account of Separation Security",\n   booktitle = "Proceedings of the 2011 International Conference on Engineering Reconfigurable Systems and Algorithms (ERSA11)",\n   author = "Gerard Allwein and William L. Harrison",\n   year = 2011,\n   url_Paper = "https://harrisonwl.github.io/assets/papers/ersa2011a.pdf",\n  abstract = "It has long been held that information flow security models should be organized with respect to a theory of information, but typically they are not. The appeal of a information-theoretic foundation for information flow security seems natural, compelling and, indeed, almost tautological. This article illustrates how channel theory---a theory of information based in logic---can provide a basis for noninterference style security models. The evidence presented here suggests that channel theory is a useful organizing principle for information flow security.",\n   }\n\n
\n
\n\n\n
\n It has long been held that information flow security models should be organized with respect to a theory of information, but typically they are not. The appeal of a information-theoretic foundation for information flow security seems natural, compelling and, indeed, almost tautological. This article illustrates how channel theory—a theory of information based in logic—can provide a basis for noninterference style security models. The evidence presented here suggests that channel theory is a useful organizing principle for information flow security.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards Semantics-directed System Design and Synthesis.\n \n \n \n \n\n\n \n Harrison, W. L.; Schulz, B.; Procter, A.; Lukefahr, A.; and Allwein, G.\n\n\n \n\n\n\n In Proceedings of the 2011 International Conference on Engineering Reconfigurable Systems and Algorithms (ERSA11), 2011. \n \n\n\n\n
\n\n\n\n \n \n \"Towards paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ERSA2011b,\n   title = "Towards Semantics-directed System Design and Synthesis",\n   booktitle = "Proceedings of the 2011 International Conference on Engineering Reconfigurable Systems and Algorithms (ERSA11)",\n   author = "William L. Harrison and Benjamin Schulz and Adam Procter and Andrew Lukefahr and Gerard Allwein",\n   year = 2011,\n      url_Paper = "https://harrisonwl.github.io/assets/papers/ersa2011b.pdf",\n  abstract = "High assurance systems have been defined as systems ``you would bet your life on.'' This article discusses the application of a form of functional programming---what we call ``monadic programming''---to the generation of high assurance and secure systems. Monadic programming languages leverage algebraic structures from denotational semantics and functional programming---monads---as a flexible, modular organizing principle for secure system design and implementation. Monadic programming languages are domain-specific functional languages that are both sufficiently expressive to express essential system behaviors and semantically straightforward to support formal verification.",\n   }   \n\n
\n
\n\n\n
\n High assurance systems have been defined as systems ``you would bet your life on.'' This article discusses the application of a form of functional programming—what we call ``monadic programming''—to the generation of high assurance and secure systems. Monadic programming languages leverage algebraic structures from denotational semantics and functional programming—monads—as a flexible, modular organizing principle for secure system design and implementation. Monadic programming languages are domain-specific functional languages that are both sufficiently expressive to express essential system behaviors and semantically straightforward to support formal verification.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Qualitative Decision Theory via Channel Theory.\n \n \n \n \n\n\n \n Allwein, G.; Yang, Y.; and Harrison, W. L.\n\n\n \n\n\n\n Logic and Logical Philosophy,81-110. 2011.\n Extended version of i̧teAllweinYangHarrison:2010\n\n\n\n
\n\n\n\n \n \n \"Qualitative paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{LLP10,\n author = "Gerard Allwein and Yingrui Yang and William L. Harrison",\n title  = "Qualitative Decision Theory via Channel Theory",\n journal = "Logic and Logical Philosophy",\n vol = 20,\n year = 2011,\n pages = {81-110},\n note = {Extended version of \\cite{AllweinYangHarrison:2010}},\n       url_Paper = "https://harrisonwl.github.io/assets/papers/llp2011.pdf",\n  abstract = "We recast parts of decision theory in terms of channel theory\nconcentrating on qualitative issues. Channel theory allows one to move\nbetween model theoretic and language theoretic notions as is necessary for\nan adequate covering. Doing so clari?es decision theory and presents the\nopportunity to investigate alternative formulations. As an example, we take\nsome of Savage's notions of decision theory and recast them within channel\ntheory. In place of probabilities, we use a particular logic of preference. We\nintroduce a logic for describing actions separate from the logic of preference\nover actions. The structures introduced by channel theory that represent\nthe decision problems can be seen to be an abstract framework. This framework is very accommodating to changing the nature of the decision problems\nto handle different aspects or theories about decision making.",\n}\n\n
\n
\n\n\n
\n We recast parts of decision theory in terms of channel theory concentrating on qualitative issues. Channel theory allows one to move between model theoretic and language theoretic notions as is necessary for an adequate covering. Doing so clari?es decision theory and presents the opportunity to investigate alternative formulations. As an example, we take some of Savage's notions of decision theory and recast them within channel theory. In place of probabilities, we use a particular logic of preference. We introduce a logic for describing actions separate from the logic of preference over actions. The structures introduced by channel theory that represent the decision problems can be seen to be an abstract framework. This framework is very accommodating to changing the nature of the decision problems to handle different aspects or theories about decision making.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Decision Theory via Channel Theory.\n \n \n \n\n\n \n Allwein, G.; Yang, Y.; and Harrison, W. S.\n\n\n \n\n\n\n In Proceedings of the Logic in Cognitive Science Conference, 2010, Logic and Logical Philosophy Journal, 2010. The Nicolaus Copernicus University Press\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inProceedings {AllweinYangHarrison:2010,\nauthor    ={Gerard Allwein and Yingrui Yang and William S. Harrison},\ntitle        ={Decision Theory via Channel Theory},\nbooktitle    ={Proceedings of the Logic in Cognitive Science Conference, 2010, Logic and Logical Philosophy Journal},\npublisher    ={The Nicolaus Copernicus University Press},\nyear        ={2010},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Partially-ordered Modalities.\n \n \n \n \n\n\n \n Allwein, G.; and Harrison, W. L.\n\n\n \n\n\n\n In Advances in Modal Logic, pages 1-21, 2010. \n \n\n\n\n
\n\n\n\n \n \n \"Partially-ordered paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{AiML10,\n  author    = {Gerard Allwein and William L. Harrison},\n  title     = {Partially-ordered Modalities},\n  booktitle = {Advances in Modal Logic},\n  year      = {2010},\n  pages     = {1-21},\n        url_Paper = "https://harrisonwl.github.io/assets/papers/aiml10.pdf",\n  abstract = "\nModal logic is extended by partially ordering the modalities. The modalities are normal, i.e., commute\nwith either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The partial\norder does not conflict with type of modality (K, S4, etc.) although this paper will concentrate on S4\nsince partially ordered S4 systems appear to be numerous. The partially-ordered normal modal systems\nconsidered are both sound and complete. Hilbert and Gentzen systems are given. A cut-elimination theorem\nholds (for partially ordered S4), and the Hilbert and Gentzen systems present the same logic. The partial\norder induces a 2-category structure on a coalgebraic formulation of descriptive frames. Channel theory is\nused to `move' modal logics when the source and target languages may be di\u000berent. A particular partially\nordered modal system is shown to be applicable to security properties",\n}\n\n
\n
\n\n\n
\n Modal logic is extended by partially ordering the modalities. The modalities are normal, i.e., commute with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The partial order does not conflict with type of modality (K, S4, etc.) although this paper will concentrate on S4 since partially ordered S4 systems appear to be numerous. The partially-ordered normal modal systems considered are both sound and complete. Hilbert and Gentzen systems are given. A cut-elimination theorem holds (for partially ordered S4), and the Hilbert and Gentzen systems present the same logic. The partial order induces a 2-category structure on a coalgebraic formulation of descriptive frames. Channel theory is used to `move' modal logics when the source and target languages may be di\u000berent. A particular partially ordered modal system is shown to be applicable to security properties\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2009\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Model-Driven Engineering from Modular Monadic Semantics: Implementation Techniques Targeting Hardware and Software.\n \n \n \n \n\n\n \n Harrison, W.; Procter, A.; Agron, J.; Kimmel, G.; and Allwein, G.\n\n\n \n\n\n\n In DSL '09: Proc. of the IFIP TC 2 Working Conference on Domain-Specific Languages, pages 20–44, 2009. \n \n\n\n\n
\n\n\n\n \n \n \"Model-Driven paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{dslwc09,\nauthor = {W. Harrison and A. Procter and J. Agron and G. Kimmel and G. Allwein},\n title = {Model-Driven Engineering from Modular Monadic Semantics: Implementation Techniques Targeting Hardware and Software},\n booktitle = {DSL '09: Proc. of the IFIP TC 2 Working Conference on Domain-Specific Languages},\n year = {2009},\n pages = {20--44},\n       url_Paper = "https://harrisonwl.github.io/assets/papers/dsl09.pdf",\n  abstract = "Recent research has shown how the formal modeling of concurrent systems can benefit from monadic structuring. With this approach, a formal system model is really a program in a domain specific language defined by a monad for shared-state concurrency. Can these models be compiled into efficient implementations?  This paper addresses this question and presents an overview of techniques for compiling monadic concurrency models directly into reasonably efficient software and hardware implementations. The implementation techniques described in this article form the basis of a semantics-directed approach to model-driven engineering.",\n } \n\n\n
\n
\n\n\n
\n Recent research has shown how the formal modeling of concurrent systems can benefit from monadic structuring. With this approach, a formal system model is really a program in a domain specific language defined by a monad for shared-state concurrency. Can these models be compiled into efficient implementations? This paper addresses this question and presents an overview of techniques for compiling monadic concurrency models directly into reasonably efficient software and hardware implementations. The implementation techniques described in this article form the basis of a semantics-directed approach to model-driven engineering.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Achieving information flow security through monadic control of effects.\n \n \n \n \n\n\n \n Harrison, W. L.; and Hook, J.\n\n\n \n\n\n\n J. Comput. Secur., 17: 599–653. October 2009.\n \n\n\n\n
\n\n\n\n \n \n \"Achieving paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{HarrisonHook09,\n author = {Harrison, William L. and Hook, James},\n title = {Achieving information flow security through monadic control of effects},\n journal = {J. Comput. Secur.},\n volume = {17},\n issue = {5},\n month = {October},\n year = {2009},\n pages = {599--653},\n numpages = {55},\n publisher = {IOS Press},\n address = {Amsterdam, The Netherlands, The Netherlands},\n       url_Paper = "https://harrisonwl.github.io/assets/papers/jcs09.pdf",\n  abstract = "This paper advocates a novel approach to the construction of secure\nsoftware: controlling information flow and maintaining integrity via\nmonadic encapsulation of effects. This approach is {\\em constructive},\nrelying on properties of monads and monad transformers to build,\nverify, and extend secure software systems. We illustrate this\napproach by construction of abstract operating systems called {\\em\n  separation kernels}. Starting from a mathematical model of\nshared-state concurrency based on monads of resumptions and state, we\noutline the development by stepwise refinements of separation kernels\nsupporting Unix-like system calls, interdomain communication,  and a\nformally verified security policy (domain separation). Because monads\nmay be easily and safely represented within any pure, higher-order,\ntyped functional language, the resulting system models may be directly\nrealized within a language such as Haskell.",\n} \n\n
\n
\n\n\n
\n This paper advocates a novel approach to the construction of secure software: controlling information flow and maintaining integrity via monadic encapsulation of effects. This approach is \\em constructive, relying on properties of monads and monad transformers to build, verify, and extend secure software systems. We illustrate this approach by construction of abstract operating systems called \\em separation kernels. Starting from a mathematical model of shared-state concurrency based on monads of resumptions and state, we outline the development by stepwise refinements of separation kernels supporting Unix-like system calls, interdomain communication, and a formally verified security policy (domain separation). Because monads may be easily and safely represented within any pure, higher-order, typed functional language, the resulting system models may be directly realized within a language such as Haskell.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2008\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Asynchronous Exceptions as an Effect.\n \n \n \n \n\n\n \n Harrison, W. L.; Allwein, G.; Gill, A.; and Procter, A.\n\n\n \n\n\n\n In Proceedings of the Mathematics of Program Construction (MPC08), pages 153–176, 2008. \n \n\n\n\n
\n\n\n\n \n \n \"Asynchronous paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{HarrisonAllwein08,\nauthor = {William L. Harrison and Gerard Allwein and Andy Gill and Adam Procter},\ntitle = {Asynchronous Exceptions as an Effect},\nbooktitle = {Proceedings of the Mathematics of Program Construction (MPC08)},\nyear = {2008},\npages = {153--176},\nnumpages = {24},\n      url_Paper = "https://harrisonwl.github.io/assets/papers/mpc08.pdf",\n  abstract = "Asynchronous interrupts abound in computing systems, yet they remain a\nthorny concept for both programming and verification practice.\nThe ubiquity of interrupts underscores the importance of developing\nprogramming models to aid the development and verification of\ninterrupt-driven programs. \nThe research reported here recognizes asynchronous interrupts as a\ncomputational effect and encapsulates them as a building block in\nmodular monadic semantics.\nThe resulting modular semantic model can serve as both a guide for\nfunctional programming with interrupts and as a formal basis for reasoning about\ninterrupt-driven computation as well.",\n}\n\n
\n
\n\n\n
\n Asynchronous interrupts abound in computing systems, yet they remain a thorny concept for both programming and verification practice. The ubiquity of interrupts underscores the importance of developing programming models to aid the development and verification of interrupt-driven programs. The research reported here recognizes asynchronous interrupts as a computational effect and encapsulates them as a building block in modular monadic semantics. The resulting modular semantic model can serve as both a guide for functional programming with interrupts and as a formal basis for reasoning about interrupt-driven computation as well.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Making monads first-class with template haskell.\n \n \n \n \n\n\n \n Kariotis, P. S.; Procter, A. M.; and Harrison, W. L.\n\n\n \n\n\n\n In Proceedings of the first ACM SIGPLAN Symposium on Haskell, of Haskell '08, pages 99–110, New York, NY, USA, 2008. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Making paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Haskell08,\n author = {Kariotis, Pericles S. and Procter, Adam M. and Harrison, William L.},\n title = {Making monads first-class with template haskell},\n booktitle = {Proceedings of the first ACM SIGPLAN Symposium on Haskell},\n series = {Haskell '08},\n year = {2008},\n location = {Victoria, BC, Canada},\n pages = {99--110},\n numpages = {12},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {domain-specific languages, monads, staged programming},\n       url_Paper = "https://harrisonwl.github.io/assets/papers/haskell08.pdf",\n  abstract = "Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.",\n} \n\n
\n
\n\n\n
\n Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2006\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Proof Abstraction for Imperative Languages.\n \n \n \n \n\n\n \n Harrison, W.\n\n\n \n\n\n\n In Proceedings of the 4th Asian Symposium on Programming Languages and Systems (APLAS06), pages 97-113, 2006. \n \n\n\n\n
\n\n\n\n \n \n \"Proof paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{APLAS06,\n  author =       "William Harrison",\n  title =        "Proof Abstraction for Imperative Languages",\n  year =         "2006",\n  booktitle = "Proceedings of the 4th Asian Symposium\n               on Programming Languages and Systems (APLAS06)",\n  pages     = {97-113}, \n  abstract = "Modularity in programming language semantics derives from abstracting over\nthe structure of underlying denotations, yielding semantic descriptions that are more abstract and reusable. One such semantic framework is Liang's modular\nmonadic semantics in which the underlying semantic structure is encapsulated with a monad. Such abstraction can be at odds with\nprogram verification, however, because program specifications require access to the (deliberately) hidden semantic\nrepresentation. The techniques for reasoning about modular monadic definitions of imperative programs introduced here overcome this barrier.\nAnd, just like program definitions in modular monadic semantics, our program specifications and proofs are representation-independent\nand hold for whole classes of monads, thereby yielding proofs of great generality.",\n  url_Paper = "https://harrisonwl.github.io/assets/papers/aplas06.pdf",\n}\n\n
\n
\n\n\n
\n Modularity in programming language semantics derives from abstracting over the structure of underlying denotations, yielding semantic descriptions that are more abstract and reusable. One such semantic framework is Liang's modular monadic semantics in which the underlying semantic structure is encapsulated with a monad. Such abstraction can be at odds with program verification, however, because program specifications require access to the (deliberately) hidden semantic representation. The techniques for reasoning about modular monadic definitions of imperative programs introduced here overcome this barrier. And, just like program definitions in modular monadic semantics, our program specifications and proofs are representation-independent and hold for whole classes of monads, thereby yielding proofs of great generality.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Essence of Multitasking.\n \n \n \n \n\n\n \n Harrison, W. L.\n\n\n \n\n\n\n In 11th International Conference on Algebraic Methodology and Software Technology (AMAST 2006), pages 158-172, July 2006. \n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n \n \"The code\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{harrison06,\n  author    = {William L. Harrison},\n  title     = {The Essence of Multitasking},\n  booktitle = {11th International Conference on Algebraic Methodology\n                  and Software Technology {(AMAST 2006)}},\n  pages     = {158-172},\n  month     = {July},                  \n  year      = {2006},\n     url_Paper = "https://harrisonwl.github.io/assets/papers/amast06.pdf",\n  abstract = "This article demonstrates how a powerful and expressive abstraction from concurrency theory---monads of resumptions---plays a dual r\\^{o}le as a programming tool\nfor concurrent applications.  \nThe article demonstrates how a\nwide variety of typical OS behaviors may be specified in terms of\nresumption monads known heretofore exclusively in the literature of \nprogramming language semantics. \nWe illustrate the expressiveness of the resumption monad with the\nconstruction of an exemplary \nmultitasking kernel in the pure functional language\nHaskell. Code available at link.",\n     url_Code = "https://harrisonwl.github.io/assets/code/EoMT.tar.gz",\n}\n\n\n\n
\n
\n\n\n
\n This article demonstrates how a powerful and expressive abstraction from concurrency theory—monads of resumptions—plays a dual rôle as a programming tool for concurrent applications. The article demonstrates how a wide variety of typical OS behaviors may be specified in terms of resumption monads known heretofore exclusively in the literature of programming language semantics. We illustrate the expressiveness of the resumption monad with the construction of an exemplary multitasking kernel in the pure functional language Haskell. Code available at link.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2005\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n RNA Pseudoknot Prediction Using Term Rewriting.\n \n \n \n\n\n \n Fu, X. Z.; Wang, H.; Harrison, W.; and Harrison, R.\n\n\n \n\n\n\n International Journal of Data Mining and Bioinformatics. 2005.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{ijdmb06,\n\tAuthor = {X. Z. Fu and H. Wang and W. Harrison and R. Harrison},\n\tTitle = {{RNA} Pseudoknot Prediction Using Term Rewriting},\n\tYear = 2005,\n  journal =      "International Journal of Data Mining and Bioinformatics",\n  abstract = "RNA plays a critical role in mediating every step of cellular information transfer from genes to functional proteins. Pseudoknots are functionally important and widely occurring structural motifs found in all types of RNA. Therefore predicting their structures is an important problem. In this paper, we present a new RNA pseudoknot structure prediction method based on term rewriting. The method is implemented using the Mfold RNA/DNA folding package and the term rewriting language Maude. In our method, RNA structures are treated as terms and rules are discovered for predicting pseudoknots. Our method was tested on 211 pseudoknots in PseudoBase and achieves an average accuracy of 74.085 percent compared to the experimentally determined structure. In fact, most pseudoknots discovered by our method achieve an accuracy of above 90 percent. These results indicate that term rewriting has a broad potential in RNA applications ranging from prediction of pseudoknots to discovery of higher level RNA structures involving complex RNA tertiary interactions."\n}\n\n                  \n
\n
\n\n\n
\n RNA plays a critical role in mediating every step of cellular information transfer from genes to functional proteins. Pseudoknots are functionally important and widely occurring structural motifs found in all types of RNA. Therefore predicting their structures is an important problem. In this paper, we present a new RNA pseudoknot structure prediction method based on term rewriting. The method is implemented using the Mfold RNA/DNA folding package and the term rewriting language Maude. In our method, RNA structures are treated as terms and rules are discovered for predicting pseudoknots. Our method was tested on 211 pseudoknots in PseudoBase and achieves an average accuracy of 74.085 percent compared to the experimentally determined structure. In fact, most pseudoknots discovered by our method achieve an accuracy of above 90 percent. These results indicate that term rewriting has a broad potential in RNA applications ranging from prediction of pseudoknots to discovery of higher level RNA structures involving complex RNA tertiary interactions.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Logic of Demand in Haskell.\n \n \n \n \n\n\n \n Harrison, W. L.; and Kieburtz, R. B.\n\n\n \n\n\n\n Journal of Functional Programming, 15(6): 837-891. 2005.\n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{HK05,\n  author =       "William L. Harrison and Richard B. Kieburtz",\n  title =        "The Logic of Demand in {H}askell",\n  journal =      "Journal of Functional Programming",\n  volume  = 15,\n  number = 6,\n  year   = 2005,\n  pages = {837-891},\n  hjournal = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/jfp05.pdf",\n  abstract = "Haskell is a functional programming language whose\n                  evaluation is lazy by default. However, Haskell also\n                  provides pattern matching facilities which add a\n                  modicum of eagerness to its otherwise lazy default\n                  evaluation. This mixed or \\emph{non-strict}\n                  semantics can be quite difficult to reason\n                  with. This paper introduces a programming logic,\n                  P-Logic, which neatly formalizes the mixed\n                  evaluation in Haskell pattern-matching as a logic,\n                  thereby simplifying the task of specifying and\n                  verifying Haskell programs. In P-Logic, aspects of\n                  demand are reflected or represented within both the\n                  predicate language and its model theory, allowing\n                  for expressive and comprehensible program\n                  verification.", \n}\n\n
\n
\n\n\n
\n Haskell is a functional programming language whose evaluation is lazy by default. However, Haskell also provides pattern matching facilities which add a modicum of eagerness to its otherwise lazy default evaluation. This mixed or \\emphnon-strict semantics can be quite difficult to reason with. This paper introduces a programming logic, P-Logic, which neatly formalizes the mixed evaluation in Haskell pattern-matching as a logic, thereby simplifying the task of specifying and verifying Haskell programs. In P-Logic, aspects of demand are reflected or represented within both the predicate language and its model theory, allowing for expressive and comprehensible program verification.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Simple Semantics for Polymorphic Recursion.\n \n \n \n \n\n\n \n Harrison, W.\n\n\n \n\n\n\n In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS05), pages 37-51, Tsukuba, Japan, November 2005. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{APLAS05,\n     author = "William Harrison",\n     title  = "A Simple Semantics for Polymorphic\n                  Recursion",\n     booktitle = "Proceedings of the 3rd Asian Symposium\n                  on Programming Languages and Systems (APLAS05)",\n     pages     = {37-51}, \n     month = "November",\n     year = 2005,\n     address = "Tsukuba, Japan",\n     hconf = "yes",\n      url_Paper = "https://harrisonwl.github.io/assets/papers/aplas05.pdf",\n     abstract = "Polymorphic recursion is a useful extension of Hindley-\nMilner typing and has been incorporated in the functional programming\nlanguage Haskell. It allows the expression of efficient algorithms\nthat take advantage of non-uniform data structures and provides key\nsupport for generic programming. However, polymorphic recursion is,\nperhaps, not as broadly understood as it could be and this, in part,\nmotivates the denotational semantics presented here. The semantics reported\nhere also contributes an essential building block to any semantics\nof Haskell: a model for first-order polymorphic recursion. Furthermore,\nHaskell-style type classes may be described within this semantic framework\nin a straightforward and intuitively appealing manner."\n}\n\n\n
\n
\n\n\n
\n Polymorphic recursion is a useful extension of Hindley- Milner typing and has been incorporated in the functional programming language Haskell. It allows the expression of efficient algorithms that take advantage of non-uniform data structures and provides key support for generic programming. However, polymorphic recursion is, perhaps, not as broadly understood as it could be and this, in part, motivates the denotational semantics presented here. The semantics reported here also contributes an essential building block to any semantics of Haskell: a model for first-order polymorphic recursion. Furthermore, Haskell-style type classes may be described within this semantic framework in a straightforward and intuitively appealing manner.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n RNA Pseudoknot Prediction Using Term Rewriting.\n \n \n \n \n\n\n \n Fu, X. Z.; Wang, H.; Harrison, W.; and Harrison, R.\n\n\n \n\n\n\n In Proceedings of IEEE Fifth Symposium on Bioinformatics and Bioengineering (BIBE05), pages 169-176, Minneapolis, MN, October 2005. \n \n\n\n\n
\n\n\n\n \n \n \"RNA paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{BIBE05,\n\tAuthor = {X. Z. Fu and H. Wang and W. Harrison and R. Harrison},\n\tBooktitle = {Proceedings of IEEE Fifth Symposium on Bioinformatics and\n  Bioengineering (BIBE05)},\n\tMonth = {October},\n\tTitle = {{RNA} Pseudoknot Prediction Using Term Rewriting},\n\tYear = {2005},\n\taddress = "Minneapolis, MN",\n\tpages = {169-176},\n        hconf = "yes",\n         url_Paper = "https://harrisonwl.github.io/assets/papers/bibe05.pdf",\t\n\tabstract = "RNA plays a critical role in mediating every step of cellular information transfer from genes to functional proteins. Pseudoknots are widely occurring structural  motifs found in all types of RNA and are also functionally important. Therefore predicting their structures is an important problem. In this paper, we present a new RNA pseudoknot prediction model based on term rewriting rather than on dynamic programming, comparative sequence analysis, or context-free grammars. The model we describe is implemented using the Mfold RNA/DNA folding package and the term rewriting language Maude. Our model was tested on 211 pseudoknots in PseudoBase and achieves an average accuracy of 74.085% compared to the experimentally determined structure. In fact, most pseudoknots discovered by our method achieve an accuracy of above 90%. These results indicate that term rewriting has a broad potential in RNA applications from prediction of pseudoknots to higher level RNA structures involving complex RNA tertiary interactions.",\n}\n\n
\n
\n\n\n
\n RNA plays a critical role in mediating every step of cellular information transfer from genes to functional proteins. Pseudoknots are widely occurring structural motifs found in all types of RNA and are also functionally important. Therefore predicting their structures is an important problem. In this paper, we present a new RNA pseudoknot prediction model based on term rewriting rather than on dynamic programming, comparative sequence analysis, or context-free grammars. The model we describe is implemented using the Mfold RNA/DNA folding package and the term rewriting language Maude. Our model was tested on 211 pseudoknots in PseudoBase and achieves an average accuracy of 74.085% compared to the experimentally determined structure. In fact, most pseudoknots discovered by our method achieve an accuracy of above 90%. These results indicate that term rewriting has a broad potential in RNA applications from prediction of pseudoknots to higher level RNA structures involving complex RNA tertiary interactions.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Achieving Information Flow Security Through Precise Control of Effects.\n \n \n \n \n\n\n \n Harrison, W.; and Hook, J.\n\n\n \n\n\n\n In 18th IEEE Computer Security Foundations Workshop (CSFW05), pages 16-30, Aix-en-Provence, France, June 2005. \n \n\n\n\n
\n\n\n\n \n \n \"Achieving paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{CSFW05,\n\tAuthor = {William Harrison and James Hook},\n\tBooktitle = {18th IEEE Computer Security Foundations Workshop (CSFW05)},\n\tMonth = {June},\n\tTitle = {Achieving Information Flow Security Through Precise Control of Effects},\n\tYear = {2005},\n\taddress = "Aix-en-Provence, France",\n\tpages = {16-30},\n        hconf = "yes",\n         url_Paper = "https://harrisonwl.github.io/assets/papers/csfw05.pdf",\t\n\tabstract = "This paper advocates controlling information flow and maintaining integrity via monadic encapsulation of effects. This approach is constructive, relying on properties of monads and monad transformers to build, verify, and extend secure software systems. We illustrate this approach by construction of abstract operating systems called separation kernels.",\n}\n\n\n\n
\n
\n\n\n
\n This paper advocates controlling information flow and maintaining integrity via monadic encapsulation of effects. This approach is constructive, relying on properties of monads and monad transformers to build, verify, and extend secure software systems. We illustrate this approach by construction of abstract operating systems called separation kernels.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2004\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Domain Specific Languages for Cellular Interactions.\n \n \n \n \n\n\n \n Harrison, W. L.; and Harrison, R. W.\n\n\n \n\n\n\n In Proceedings of the 26th Annual IEEE International Conference on Engineering in Medicine and Biology (EMBC04), September 2004. \n \n\n\n\n
\n\n\n\n \n \n \"Domain paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{HarrisonHarrison04,\n  author =       "William L. Harrison and Robert W. Harrison",\n  title =        "Domain Specific Languages for Cellular Interactions",\n  booktitle =    "Proceedings of the 26th Annual IEEE International Conference on Engineering in Medicine and Biology (EMBC04)",\n  month =        "September",\n  year =         "2004",\n  hconf = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/embc04.pdf",\n  abstract = "Bioinformatics is the application of Computer Science techniques to problems in Biology, and this paper explores one such application with great potential: the modeling of life cycles of autonomous, intercommunicating cellular systems using domain-specific programming languages (DSLs). We illustrate this approach for the simple photo-synthetic bacterium \\emph{R. Sphaeroides} with a DSL called CellSys embedded in the programming language Haskell."\n}\n\n\n
\n
\n\n\n
\n Bioinformatics is the application of Computer Science techniques to problems in Biology, and this paper explores one such application with great potential: the modeling of life cycles of autonomous, intercommunicating cellular systems using domain-specific programming languages (DSLs). We illustrate this approach for the simple photo-synthetic bacterium \\emphR. Sphaeroides with a DSL called CellSys embedded in the programming language Haskell.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2003\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Domain Separation by Construction.\n \n \n \n \n\n\n \n Harrison, W.; Tullsen, M.; and Hook, J.\n\n\n \n\n\n\n In LICS03 Satellite Workshop on Foundations of Computer Security (FCS03), June 2003. \n 21 pages\n\n\n\n
\n\n\n\n \n \n \"Domain paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{DomSep03,\n  author =       "William Harrison and Mark Tullsen and James Hook",\n  title =        "Domain Separation by Construction",\n  booktitle =    "LICS03 Satellite Workshop on Foundations of Computer Security (FCS03)",\n  month =        "June",\n  year =         "2003",\n  note = "21 pages",\n  hconf = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/fcs03.pdf",\n  abstract = "This paper advocates a novel approach to language-based security: by structuring software with monads (a form of abstract data type for effects), we are able to maintain separation of effects by construction. The thesis of this work is that well-understood properties of monads and monad transformers aid in the construction and verification of secure software. We introduce a formulation of non-interference based on monads rather than the typical trace-based formulation. Using this formulation, we prove a non-interference style property for a simple instance of our system model. Because monads may be easily and safely represented within any pure, higher-order, typed functional language, the resulting system models may be directly realized within such a language.",\n}\n\n\n
\n
\n\n\n
\n This paper advocates a novel approach to language-based security: by structuring software with monads (a form of abstract data type for effects), we are able to maintain separation of effects by construction. The thesis of this work is that well-understood properties of monads and monad transformers aid in the construction and verification of secure software. We introduce a formulation of non-interference based on monads rather than the typical trace-based formulation. Using this formulation, we prove a non-interference style property for a simple instance of our system model. Because monads may be easily and safely represented within any pure, higher-order, typed functional language, the resulting system models may be directly realized within such a language.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2002\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Pattern-driven Reduction in Haskell.\n \n \n \n \n\n\n \n Harrison, W.; and Kieburtz, R.\n\n\n \n\n\n\n In 2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS02), Copenhagen, Denmark, 2002. \n \n\n\n\n
\n\n\n\n \n \n \"Pattern-driven paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{HK02,\n   author = "William Harrison and Richard Kieburtz",\n   title  = "Pattern-driven Reduction in Haskell",\n   booktitle = "2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS02)",\n   address = "Copenhagen, Denmark",\n   year  = "2002",\n   hconf = "yes",\n    url_Paper = "https://harrisonwl.github.io/assets/papers/wrs02.pdf",\n   abstract = "Haskell is a functional programming language with nominally non-strict\nsemantics, implying that evaluation of a Haskell expression proceeds by\ndemand-driven reduction.  However, Haskell also provides pattern \nmatching\non arguments of functions, in {\\bf let} expressions and in the match\nclauses of {\\bf case} expressions.  Pattern-matching requires\ndata-driven reduction to the extent necessary to\nevaluate a pattern match or to bind variables introduced in a pattern.\nIn this paper we\nprovide both an abstract semantics and a logical characterization of\npattern-matching in Haskell and the reduction order that it entails.",\n}\n\n\n\n
\n
\n\n\n
\n Haskell is a functional programming language with nominally non-strict semantics, implying that evaluation of a Haskell expression proceeds by demand-driven reduction. However, Haskell also provides pattern matching on arguments of functions, in \\bf let expressions and in the match clauses of \\bf case expressions. Pattern-matching requires data-driven reduction to the extent necessary to evaluate a pattern match or to bind variables introduced in a pattern. In this paper we provide both an abstract semantics and a logical characterization of pattern-matching in Haskell and the reduction order that it entails.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Fine Control of Demand in Haskell.\n \n \n \n \n\n\n \n Harrison, W.; Sheard, T.; and Hook, J.\n\n\n \n\n\n\n In 6th International Conference on the Mathematics of Program Construction (MPC02), Dagstuhl, Germany, volume 2386, of Lecture Notes in Computer Science, pages 68–93, 2002. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Fine paper\n  \n \n \n \"Fine slides\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{FCDH2002,\n  author =       "William Harrison and Timothy Sheard and James Hook",\n  title =        "Fine Control of Demand in {Haskell}",\n  booktitle =    "6th International Conference on the Mathematics of\n                 Program Construction (MPC02),\n                 Dagstuhl, Germany",\n  year =         "2002",\n  publisher =    "Springer-Verlag",\n  volume =       "2386",\n  pages =        "68--93",\n  series =       "Lecture Notes in Computer Science",\n  hconf = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/mpc02.pdf",\n   url_Slides = "https://harrisonwl.github.io/assets/papers/slides-mpc02.pdf",\n  abstract = "Functional languages have the lambda calculus at their core, but then depart from this firm foundation by including features that alter their default evaluation order. The resulting mixed evaluation---partly lazy and partly strict---complicates the formal semantics of these languages. The functional language Haskell is such a language, with features such as pattern-matching, case expressions with guards, etc., introducing a modicum of strictness into the otherwise lazy language. But just how does Haskell differ from the lazy lambda calculus? We answer this question by introducing a calculational semantics for Haskell that exposes the interaction of its strict features with its default laziness. In the semantics, features perturbing Haskell's standard lazy evaluation order are specified computationally (i.e., monadically) rather than as pure values (i.e., functions, scalars, etc.)."\n}\n\n\n\n
\n
\n\n\n
\n Functional languages have the lambda calculus at their core, but then depart from this firm foundation by including features that alter their default evaluation order. The resulting mixed evaluation—partly lazy and partly strict—complicates the formal semantics of these languages. The functional language Haskell is such a language, with features such as pattern-matching, case expressions with guards, etc., introducing a modicum of strictness into the otherwise lazy language. But just how does Haskell differ from the lazy lambda calculus? We answer this question by introducing a calculational semantics for Haskell that exposes the interaction of its strict features with its default laziness. In the semantics, features perturbing Haskell's standard lazy evaluation order are specified computationally (i.e., monadically) rather than as pure values (i.e., functions, scalars, etc.).\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2001\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Dynamically Adaptable Software with Metacomputations in a Staged Language.\n \n \n \n \n\n\n \n Harrison, B.; and Sheard, T.\n\n\n \n\n\n\n In Proceedings of the Second International Workshop on Semantics, Applications, and Implementation of Program Generation (SAIG), volume 2196, of Lecture Notes in Computer Science, pages 163–182, Florence, Italy, 2001. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Dynamically paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{HarrisonSheard2001,\n  author =       "Bill Harrison and Tim Sheard",\n  title =        "Dynamically Adaptable Software with Metacomputations in a Staged Language",\n  journal =      "Lecture Notes in Computer Science",\n  booktitle =    "Proceedings of the Second International Workshop on\n                  Semantics, Applications, and Implementation of Program Generation (SAIG)",\n  address =      "Florence, Italy", \n  volume =       "2196",\n  pages =        "163--182",\n  publisher =    "Springer-Verlag",\n  series =       "Lecture Notes in Computer Science",\n  year =         "2001",\n  hconf = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/saig01.pdf",\n  abstract = "Profile-driven compiler optimizations take advantage of information gathered at runtime to re-compile programs into more efficient code. Such optimizations appear to be more easily incorporated within a semantics-directed compiler structure than within traditional compiler structure. We present a case study in which a metacomputation-based reference compiler for a small imperative language converts easily into a compiler which performs a particular profile-driven optimization: local register allocation. Our reference compiler is implemented in the staged, functional language MetaML and takes full advantage of the synergy between metacomputation-style language definitions and the staging constructs of MetaML. We believe that the approach to implementing profile-driven optimizations presented here suggests a useful, formal model for dynamically adaptable software.",\n}\n\n
\n
\n\n\n
\n Profile-driven compiler optimizations take advantage of information gathered at runtime to re-compile programs into more efficient code. Such optimizations appear to be more easily incorporated within a semantics-directed compiler structure than within traditional compiler structure. We present a case study in which a metacomputation-based reference compiler for a small imperative language converts easily into a compiler which performs a particular profile-driven optimization: local register allocation. Our reference compiler is implemented in the staged, functional language MetaML and takes full advantage of the synergy between metacomputation-style language definitions and the staging constructs of MetaML. We believe that the approach to implementing profile-driven optimizations presented here suggests a useful, formal model for dynamically adaptable software.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modular Compilers and Their Correctness Proofs.\n \n \n \n \n\n\n \n Harrison, W.\n\n\n \n\n\n\n Ph.D. Thesis, University of Illinois at Urbana-Champaign, 2001.\n \n\n\n\n
\n\n\n\n \n \n \"Modular paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@PhdThesis{Harrison2001,\n  author =       "William Harrison",\n  title =        "Modular Compilers and Their Correctness Proofs",\n  year =         "2001",\n  school =       "University of Illinois at Urbana-Champaign",\n  hthesis = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/dissertation.pdf",\n  abstract = "This thesis explores the construction and correctness of modular compilers. Modular compilation is a compiler construction technique allowing the construction of compilers for high-level programming languages from reusable compiler building blocks. Modular compilers are defined in terms of denotational semantics based on monads, monad transformers, and a new model of staged computation called metacomputations. A novel form of denotational specification called observational program specification and related proof techniques are developed to assist in modular compiler verification. It will be demonstrated that the modular compilation framework provides both a level of modularity in compiler proofs as well as a useful organizing principle for such proofs.",\n}\n\n\n\n\n\n
\n
\n\n\n
\n This thesis explores the construction and correctness of modular compilers. Modular compilation is a compiler construction technique allowing the construction of compilers for high-level programming languages from reusable compiler building blocks. Modular compilers are defined in terms of denotational semantics based on monads, monad transformers, and a new model of staged computation called metacomputations. A novel form of denotational specification called observational program specification and related proof techniques are developed to assist in modular compiler verification. It will be demonstrated that the modular compilation framework provides both a level of modularity in compiler proofs as well as a useful organizing principle for such proofs.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2000\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Metacomputation-based Compiler Architecture.\n \n \n \n \n\n\n \n Harrison, W.; and Kamin, S.\n\n\n \n\n\n\n In 5th International Conference on the Mathematics of Program Construction, Ponte de Lima, Portugal, volume 1837, of Lecture Notes in Computer Science, pages 213–229, 2000. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Metacomputation-based paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{HarrisonKamin2000,\n  author =       "William Harrison and Samuel Kamin",\n  title =        "Metacomputation-based Compiler Architecture",\n  booktitle =    "5th International Conference on the Mathematics of\n                 Program Construction,\n                 Ponte de Lima, Portugal",\n  year =         "2000",\n  publisher =    "Springer-Verlag",\n  volume =       "1837",\n  pages =        "213--229",\n  series =       "Lecture Notes in Computer Science",\n  hconf = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/mpc00.pdf",\n  abstract = "This paper presents a modular and extensible style of language specification based on metacomputations. This style uses two monads to factor the static and dynamic parts of the specification, thereby staging the specification and achieving strong binding-time separation. Because metacomputations are defined in terms of monads, they can be constructed modularly and extensibly using monad transformers. Consequently, metacomputation-style specifications are modular and extensible. A number of language constructs are specified: expressions, control-flow, imperative features, block structure, and higher-order functions and recursive bindings. Because of the strong binding-time separation, metacomputation-style specification lends itself to semantics-directed compilation, which we demonstrate by creating a modular compiler for a block-structured imperative, while language.",\n}\n\n\n
\n
\n\n\n
\n This paper presents a modular and extensible style of language specification based on metacomputations. This style uses two monads to factor the static and dynamic parts of the specification, thereby staging the specification and achieving strong binding-time separation. Because metacomputations are defined in terms of monads, they can be constructed modularly and extensibly using monad transformers. Consequently, metacomputation-style specifications are modular and extensible. A number of language constructs are specified: expressions, control-flow, imperative features, block structure, and higher-order functions and recursive bindings. Because of the strong binding-time separation, metacomputation-style specification lends itself to semantics-directed compilation, which we demonstrate by creating a modular compiler for a block-structured imperative, while language.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1998\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Modular Compilers Based on Monad Transformers.\n \n \n \n \n\n\n \n Harrison, W. L.; and Kamin, S. N.\n\n\n \n\n\n\n In Proceedings of the 1998 International Conference on Computer Languages, pages 122–131, 1998. IEEE Computer Society Press\n \n\n\n\n
\n\n\n\n \n \n \"Modular paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{HarrisonKamin1998,\n  author =       "William L. Harrison and Samuel N. Kamin",\n  title =        "Modular Compilers Based on Monad Transformers",\n  booktitle =    "Proceedings of the 1998 International Conference on\n                 Computer Languages",\n  publisher =    "IEEE Computer Society Press",\n  year =         "1998",\n  ISBN =         "0-780-35005-7, 0-8186-8454-2, 0-8186-8456-9",\n  pages =        "122--131",\n  hconf = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/iccl98.pdf",\n  abstract =     "The monadic style of language specification has the\n                 advantages of modularity and extensibility: it is\n                 simple to add or change features in an interpreter to\n                 re ect modifications in the source language. It has\n                 proven difficult to extend the method to compilation.\n                 We demonstrate that by introducing machine-like stores\n                 (code and data) into the monadic semantics and then\n                 partially evaluating the resulting semantic\n                 expressions, we can achieve many of the same advantages\n                 for a compiler as for an interpreter. A number of\n                 language constructs and features are compiled:\n                 expressions, CBV and CBN evaluation of\n                 $\\lambda$-expressions, dynamic scoping, and various\n                 imperative features. The treatment of recursive\n                 procedures is outlined as well. The resulting method\n                 allows compilers to be constructed in a mix-and-match\n                 fashion just as in a monad-structured interpreter.",\n}\n\n
\n
\n\n\n
\n The monadic style of language specification has the advantages of modularity and extensibility: it is simple to add or change features in an interpreter to re ect modifications in the source language. It has proven difficult to extend the method to compilation. We demonstrate that by introducing machine-like stores (code and data) into the monadic semantics and then partially evaluating the resulting semantic expressions, we can achieve many of the same advantages for a compiler as for an interpreter. A number of language constructs and features are compiled: expressions, CBV and CBN evaluation of $λ$-expressions, dynamic scoping, and various imperative features. The treatment of recursive procedures is outlined as well. The resulting method allows compilers to be constructed in a mix-and-match fashion just as in a monad-structured interpreter.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1992\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL.\n \n \n \n \n\n\n \n Harrison, W.\n\n\n \n\n\n\n Master's thesis, University of California, Davis, 1992.\n \n\n\n\n
\n\n\n\n \n \n \"Mechanizing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@MastersThesis{Harrison1992,\n  author =       "William Harrison",\n  title =        "Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL",\n  year =         "1992",\n  school =       "University of California, Davis",\n  hthesis = "yes",\n   url_Paper = "https://harrisonwl.github.io/assets/papers/masters-thesis.pdf",\n  abstract = "This thesis presents the axiomatic semantics for a simple distributed language and its mechanization in HOL. The constructs of this language include asynchronous send and synchronous receive statements as well as those basic to a sequential programming language. The language has the appearance of a system programming language that supports sequential execution extended with message-passing, and would be a suitable basis for coding distributed operating systems. Included in the mechanization are functions which generate the goals associated with the verification of simple statements in the language.",\n}\n\n  \n\n\n
\n
\n\n\n
\n This thesis presents the axiomatic semantics for a simple distributed language and its mechanization in HOL. The constructs of this language include asynchronous send and synchronous receive statements as well as those basic to a sequential programming language. The language has the appearance of a system programming language that supports sequential execution extended with message-passing, and would be a suitable basis for coding distributed operating systems. Included in the mechanization are functions which generate the goals associated with the verification of simple statements in the language.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An HOL Mechanization of the Axiomatic Semantics of a Simple Distributed Programming Language.\n \n \n \n\n\n \n Harrison, W.; Levitt, K.; and Archer, M.\n\n\n \n\n\n\n In Proceedings of the International Workshop on Higher-Order Logic Theorem Proving and Its Applications, pages 347-358, Leuven, Belgium, September 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{harrison92,\n  author =       "William Harrison and Karl Levitt and Myla Archer",\n  title =        "An HOL Mechanization of the Axiomatic Semantics of a Simple\nDistributed Programming Language",\n  booktitle =    "Proceedings of the International Workshop on Higher-Order Logic\n  Theorem Proving and Its Applications",\n  month = "September",\n  address = "Leuven, Belgium",\n  year =         "1992",\n  pages =        "347-358",\n  hconf = "yes",\n  abstract = "",\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Towards a Verified Code Basis for a Secure Distributed Operating System.\n \n \n \n\n\n \n Harrison, W.; Levitt, K.; and Archer, M.\n\n\n \n\n\n\n Technical Report CSE-92-19, University of California at Davis, 1992.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@TechReport{tr92a,\n  author = \t {William Harrison and Karl Levitt and Myla Archer},\n  title = \t {{Towards a Verified Code Basis for a Secure Distributed Operating System}},\n  institution =  {University of California at Davis},\n  number =       "CSE-92-19",\n  year = \t 1992,\n  htr =          "yes",\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL.\n \n \n \n\n\n \n Harrison, W.\n\n\n \n\n\n\n Technical Report CSE-92-20, University of California at Davis, 1992.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@TechReport{tr92b,\n  author = \t {William Harrison},\n  title = \t {{Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL}},\n  institution =  {University of California at Davis},\n  number =       "CSE-92-20",\n  year = \t 1992,\n  htr =          "yes",\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1991\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Mechanizing Security in HOL.\n \n \n \n\n\n \n Harrison, W.; and Levitt, K.\n\n\n \n\n\n\n In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 63–66, Davis, California, 1991. IEEE Computer Society Press\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@INPROCEEDINGS{MeSeHOL,\n  AUTHOR = {William Harrison and Karl Levitt},\n  TITLE = {Mechanizing Security in {HOL}},\n  BOOKTITLE = {Proceedings of the 1991 International Workshop\n            on the {HOL} Theorem Proving System and its Applications},\n  PUBLISHER = {IEEE Computer Society Press},\n  YEAR = {1991},\n  PAGES = {63--66},\n  address = "Davis, California",\n  hconf = "yes",\n  abstract = "",\n}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);