Generative Unbinding of Names
This paper is concerned with the form of typed name binding used by the FreshML family of languages. Its characteristic feature is that a name binding is represented by an abstract (name,value)-pair that may only be deconstructed via the generation of fresh bound names. The paper proves a new result...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2008-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/916/pdf |
| _version_ | 1827323004611198976 |
|---|---|
| author | Andrew M. Pitts Mark R. Shinwell |
| author_facet | Andrew M. Pitts Mark R. Shinwell |
| author_sort | Andrew M. Pitts |
| collection | DOAJ |
| description | This paper is concerned with the form of typed name binding used by the
FreshML family of languages. Its characteristic feature is that a name binding
is represented by an abstract (name,value)-pair that may only be deconstructed
via the generation of fresh bound names. The paper proves a new result about
what operations on names can co-exist with this construct. In FreshML the only
observation one can make of names is to test whether or not they are equal.
This restricted amount of observation was thought necessary to ensure that
there is no observable difference between alpha-equivalent name binders. Yet
from an algorithmic point of view it would be desirable to allow other
operations and relations on names, such as a total ordering. This paper shows
that, contrary to expectations, one may add not just ordering, but almost any
relation or numerical function on names without disturbing the fundamental
correctness result about this form of typed name binding (that object-level
alpha-equivalence precisely corresponds to contextual equivalence at the
programming meta-level), so long as one takes the state of dynamically created
names into account. |
| first_indexed | 2024-04-25T01:37:52Z |
| format | Article |
| id | doaj.art-9482d57630c24174a42c9654d2a20bcc |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:52Z |
| publishDate | 2008-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-9482d57630c24174a42c9654d2a20bcc2024-03-08T08:52:02ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742008-03-01Volume 4, Issue 110.2168/LMCS-4(1:4)2008916Generative Unbinding of NamesAndrew M. Pittshttps://orcid.org/0000-0001-7775-3471Mark R. ShinwellThis paper is concerned with the form of typed name binding used by the FreshML family of languages. Its characteristic feature is that a name binding is represented by an abstract (name,value)-pair that may only be deconstructed via the generation of fresh bound names. The paper proves a new result about what operations on names can co-exist with this construct. In FreshML the only observation one can make of names is to test whether or not they are equal. This restricted amount of observation was thought necessary to ensure that there is no observable difference between alpha-equivalent name binders. Yet from an algorithmic point of view it would be desirable to allow other operations and relations on names, such as a total ordering. This paper shows that, contrary to expectations, one may add not just ordering, but almost any relation or numerical function on names without disturbing the fundamental correctness result about this form of typed name binding (that object-level alpha-equivalence precisely corresponds to contextual equivalence at the programming meta-level), so long as one takes the state of dynamically created names into account.https://lmcs.episciences.org/916/pdfcomputer science - programming languagescomputer science - logic in computer scienced.3.1d.3.3f.3.2 |
| spellingShingle | Andrew M. Pitts Mark R. Shinwell Generative Unbinding of Names Logical Methods in Computer Science computer science - programming languages computer science - logic in computer science d.3.1 d.3.3 f.3.2 |
| title | Generative Unbinding of Names |
| title_full | Generative Unbinding of Names |
| title_fullStr | Generative Unbinding of Names |
| title_full_unstemmed | Generative Unbinding of Names |
| title_short | Generative Unbinding of Names |
| title_sort | generative unbinding of names |
| topic | computer science - programming languages computer science - logic in computer science d.3.1 d.3.3 f.3.2 |
| url | https://lmcs.episciences.org/916/pdf |
| work_keys_str_mv | AT andrewmpitts generativeunbindingofnames AT markrshinwell generativeunbindingofnames |