Conference item icon

Conference item

ML and Extended Branching VASS

Abstract:

We prove that the observational equivalence problem for a finitary fragment of ML is recursively equivalent to the reachability problem for extended branching vector addition systems with states (EBVASS). Our proof uses the fully abstract game semantics of the language. We introduce a new class of automata, VPCMA, as a representation of the game semantics. VPCMA are a version of class memory automata equipped with a visibly pushdown stack; they serve as a bridge enabling interreducibility of ...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-662-54434-1_12

Authors


More by this author
Institution:
University of Oxford
Oxford college:
Balliol College
Role:
Author
More by this author
Institution:
University of Oxford
Oxford college:
Merton College
Role:
Author
Publisher:
Springer Publisher's website
Journal:
26th European Symposium on Programming (ESOP'17) Journal website
Host title:
26th European Symposium on Programming (ESOP'17)
Publication date:
2017-03-01
Acceptance date:
2017-02-25
DOI:
Source identifiers:
685452
Pubs id:
pubs:685452
UUID:
uuid:f8b46a05-9363-4b33-9c17-2f2f42e03340
Local pid:
pubs:685452
Deposit date:
2017-03-12

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP