The Library
Fragments of ML decidable by nested data class memory automata
Tools
Cotton-Barratt, Conrad, Hopkins, David (Computer scientist), Murawski, Andrzej S. and Ong, Luke (2015) Fragments of ML decidable by nested data class memory automata. In: Pitts, Andrew, (ed.) Foundations of software science and computation structures : 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. Lecture Notes in Computer Science (Volume 9034). Berlin ; Heidelberg: Springer, pp. 249-263. ISBN 9783662466773
|
PDF
WRAP_1271755-cs-090715-paper_35.pdf - Accepted Version - Requires a PDF viewer. Download (686Kb) | Preview |
Official URL: http://dx.doi.org/10.1007/978-3-662-46678-0_16
Abstract
The call-by-value language RML may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a “bad variable” construct in the sense of Reynolds. We consider the fragment of (finitary) RML terms of order at most 1 with free variables of order at most 2, and identify two subfragments of this for which we show observational equivalence to be decidable. The first subfragment, RMLP−Str2⊢1, consists of those terms in which the P-pointers in the game semantic representation are determined by the underlying sequence of moves. The second subfragment consists of terms in which the O-pointers of moves corresponding to free variables in the game semantic representation are determined by the underlying moves. These results are shown using a reduction to a form of automata over data words in which the data values have a tree-structure, reflecting the tree-structure of the threads in the game semantic plays. In addition we show that observational equivalence is undecidable at every third- or higher-order type, every second-order type which takes at least two first-order arguments, and every second-order type (of arity greater than one) that has a first-order argument which is not the final argument.
Item Type: | Book Item | ||||||
---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
Library of Congress Subject Headings (LCSH): | ML (Computer program language) | ||||||
Series Name: | Lecture Notes in Computer Science | ||||||
Publisher: | Springer | ||||||
Place of Publication: | Berlin ; Heidelberg | ||||||
ISBN: | 9783662466773 | ||||||
ISSN: | 0302-9743 | ||||||
Book Title: | Foundations of software science and computation structures : 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings | ||||||
Editor: | Pitts, Andrew | ||||||
Official Date: | 2015 | ||||||
Dates: |
|
||||||
Number: | Volume 9034 | ||||||
Page Range: | pp. 249-263 | ||||||
DOI: | 10.1007/978-3-662-46678-0_16 | ||||||
Status: | Peer Reviewed | ||||||
Publication Status: | Published | ||||||
Access rights to Published version: | Restricted or Subscription Access | ||||||
Date of first compliant deposit: | 30 December 2015 | ||||||
Date of first compliant Open Access: | 28 May 2016 | ||||||
Funder: | Engineering and Physical Sciences Research Council (EPSRC), Microsoft Research, Ensoft, Inc., Merton College | ||||||
Grant number: | EP/J019577/1 (EPSRC) |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year