@MastersThesis{Harrison1992,
  author =       "William Harrison",
  title =        "Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL",
  year =         "1992",
  school =       "University of California, Davis",
  hthesis = "yes",
   url_Paper = "https://harrisonwl.github.io/assets/papers/masters-thesis.pdf",
  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.",
}

{"_id":"EMYyZYftDi9ZCoQGb","bibbaseid":"harrison-mechanizingtheaxiomaticsemanticsforaprogramminglanguagewithasynchronoussendandreceiveinhol-1992","downloads":1,"creationDate":"2016-07-28T19:31:33.389Z","title":"Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL","author_short":["Harrison, W."],"year":1992,"bibtype":"mastersthesis","biburl":"https://harrisonwl.github.io/assets/bibliography/harrison.bib","bibdata":{"bibtype":"mastersthesis","type":"mastersthesis","author":[{"firstnames":["William"],"propositions":[],"lastnames":["Harrison"],"suffixes":[]}],"title":"Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL","year":"1992","school":"University of California, Davis","hthesis":"yes","url_paper":"https://harrisonwl.github.io/assets/papers/masters-thesis.pdf","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.","bibtex":"@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","author_short":["Harrison, W."],"key":"Harrison1992","id":"Harrison1992","bibbaseid":"harrison-mechanizingtheaxiomaticsemanticsforaprogramminglanguagewithasynchronoussendandreceiveinhol-1992","role":"author","urls":{" paper":"https://harrisonwl.github.io/assets/papers/masters-thesis.pdf"},"metadata":{"authorlinks":{"harrison, w":"https://harrisonwl.github.io/etc/publications.html"}},"downloads":1},"search_terms":["mechanizing","axiomatic","semantics","programming","language","asynchronous","send","receive","hol","harrison"],"keywords":[],"authorIDs":["iCiuqX2A39oLpzRv9"],"dataSources":["wAeScLDKnpPTHdYwg","uCveoExKMHQNZnZCp"]}