Computing with Contexts: A simple approach. Sands, D. In Gordon, A. D., Pitts, A. M., & Talcott, C. L., editors, *Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II)*, volume 10, of *Electronic Notes in Theoretical Computer Science*. Elsevier Science Publishers B.V., 1998. Paper abstract bibtex This article describes how the use of a higher-order syntax representation of contexts [due to A. Pitts] combines smoothly with higher-order syntax for evaluation rules, so that definitions can be extended to work over contexts. This provides "for free" - without the development of any new language-specific context calculi - evaluation rules for contexts which commute with hole-filling. We have found this to be a useful technique for directly reasoning about operational equivalence. A small illustration is given based on a unique fixed-point induction principle for a notion of guarded context in a functional language.

@INCOLLECTION{Sands:Computing,
author = {David Sands},
title = {Computing with Contexts: {A} simple approach},
booktitle = {Second Workshop on Higher-Order Operational Techniques in
Semantics (HOOTS II)},
editor = {A. D. Gordon and A. M. Pitts and C. L. Talcott},
series = {Electronic Notes in Theoretical Computer Science},
year = {1998},
volume = {10},
publisher = {Elsevier Science Publishers B.V.},
url_Paper = {http://www.cse.chalmers.se/~dave/papers/ENTCS10-sands.pdf},
abstract = {This article describes how the use of a higher-order syntax
representation of contexts [due to A. Pitts] combines smoothly with
higher-order syntax for evaluation rules, so that definitions can be
extended to work over contexts. This provides "for free" - without the
development of any new language-specific context calculi - evaluation rules
for contexts which commute with hole-filling. We have found this to be a
useful technique for directly reasoning about operational equivalence. A
small illustration is given based on a unique fixed-point induction
principle for a notion of guarded context in a functional language.},
}

Downloads: 0

{"_id":"ZjwvdL27hru5xFEWv","bibbaseid":"sands-computingwithcontextsasimpleapproach-1998","downloads":0,"creationDate":"2017-02-03T08:24:26.834Z","title":"Computing with Contexts: A simple approach","author_short":["Sands, D."],"year":1998,"bibtype":"incollection","biburl":"http://www.cse.chalmers.se/~dave/davewww2016.bib","bibdata":{"bibtype":"incollection","type":"incollection","author":[{"firstnames":["David"],"propositions":[],"lastnames":["Sands"],"suffixes":[]}],"title":"Computing with Contexts: A simple approach","booktitle":"Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II)","editor":[{"firstnames":["A.","D."],"propositions":[],"lastnames":["Gordon"],"suffixes":[]},{"firstnames":["A.","M."],"propositions":[],"lastnames":["Pitts"],"suffixes":[]},{"firstnames":["C.","L."],"propositions":[],"lastnames":["Talcott"],"suffixes":[]}],"series":"Electronic Notes in Theoretical Computer Science","year":"1998","volume":"10","publisher":"Elsevier Science Publishers B.V.","url_paper":"http://www.cse.chalmers.se/~dave/papers/ENTCS10-sands.pdf","abstract":"This article describes how the use of a higher-order syntax representation of contexts [due to A. Pitts] combines smoothly with higher-order syntax for evaluation rules, so that definitions can be extended to work over contexts. This provides \"for free\" - without the development of any new language-specific context calculi - evaluation rules for contexts which commute with hole-filling. We have found this to be a useful technique for directly reasoning about operational equivalence. A small illustration is given based on a unique fixed-point induction principle for a notion of guarded context in a functional language.","bibtex":"@INCOLLECTION{Sands:Computing,\n author = {David Sands},\n title = {Computing with Contexts: {A} simple approach},\n booktitle = {Second Workshop on Higher-Order Operational Techniques in\n Semantics (HOOTS II)},\n editor = {A. D. Gordon and A. M. Pitts and C. L. Talcott},\n series = {Electronic Notes in Theoretical Computer Science},\n year = {1998},\n volume = {10},\n publisher = {Elsevier Science Publishers B.V.},\n url_Paper = {http://www.cse.chalmers.se/~dave/papers/ENTCS10-sands.pdf},\n abstract = {This article describes how the use of a higher-order syntax\nrepresentation of contexts [due to A. Pitts] combines smoothly with\nhigher-order syntax for evaluation rules, so that definitions can be\nextended to work over contexts. This provides \"for free\" - without the\ndevelopment of any new language-specific context calculi - evaluation rules\nfor contexts which commute with hole-filling. We have found this to be a\nuseful technique for directly reasoning about operational equivalence. A\nsmall illustration is given based on a unique fixed-point induction\nprinciple for a notion of guarded context in a functional language.},\n}\n\n","author_short":["Sands, D."],"editor_short":["Gordon, A. D.","Pitts, A. M.","Talcott, C. L."],"key":"Sands:Computing","id":"Sands:Computing","bibbaseid":"sands-computingwithcontextsasimpleapproach-1998","role":"author","urls":{" paper":"http://www.cse.chalmers.se/~dave/papers/ENTCS10-sands.pdf"},"downloads":0},"search_terms":["computing","contexts","simple","approach","sands"],"keywords":[],"authorIDs":["58943e3a2f18920f4c000022"],"dataSources":["SBHWXKotbthoEYKJv"]}