We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Complete trace models of state and control

Authors: Guilhem Jaber (GALLINETTE, LS2N), Andrzej S. Murawski
Abstract: We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either callcc or no control operator.Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-order references and callcc, constructed in the spirit of operational game semantics. Next we examine the impact of suppressing higher-order references and callcc in contexts and provide an operational explanation for the game-semantic conditions known as visibility and bracketing respectively.This allows us to refine the original model to provide fully abstract trace models of interaction with contexts that need not use higher-order references or callcc. Along the way, we discuss the relationship between error- and termination-based contextual testing in each case, and relate the two to trace and complete trace equivalence respectively.Overall, the paper provides a systematic development of operational game semantics for all four cases, which represent the state-based face of the so-called semantic cube.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Cite as: arXiv:2101.08491 [cs.LO]
  (or arXiv:2101.08491v1 [cs.LO] for this version)

Submission history

From: Guilhem Jaber [view email]
[v1] Thu, 21 Jan 2021 08:11:08 GMT (80kb)

Link back to: arXiv, form interface, contact.