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"]}