| Autor: |
Murawski AS; 1University of Warwick, Coventry, UK., Tzevelekos N; 2Queen Mary University of London, London, UK. |
| Jazyk: |
angličtina |
| Zdroj: |
Formal methods in system design [Form Methods Syst Des] 2018; Vol. 52 (3), pp. 277-314. Date of Electronic Publication: 2017 Aug 09. |
| DOI: |
10.1007/s10703-017-0292-9 |
| Abstrakt: |
We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is unit → unit → unit . At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation. |
| Databáze: |
MEDLINE |
| Externí odkaz: |
|
Full text from SpringerLink