tag:blogger.com,1999:blog-11162230.post2986543708646345175..comments2024-03-04T13:50:45.089-08:00Comments on Jeremy Siek: Over-specification in operational semantics, or the case of the missing "eval"Jeremy Siekhttp://www.blogger.com/profile/13773635290126992920noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-11162230.post-10472167330983287942012-07-16T09:26:52.216-07:002012-07-16T09:26:52.216-07:00Yes, once we start talking about languages with in...Yes, once we start talking about languages with input and output, then the notion of observation must be some form of trace. And once we start talking about separate compilation and ABIs (application binary interfaces), we need a more detailed kind of trace. I see several different formalisms out there that might do the job: the testing semantics from concurrent calculi (e.g. <i>Algebraic Theory of Processes</i> by Matthew Hennessy),<br />game semantics (e.g. work by Samson Abramsky, Luke Ong, etc.), and decision trees for SPCF (Cartwright, Felleisen, Berry, and Curien). I think the real trick will be distilling the simplest form of such semantics and relating them to more familiar operational semantics, so that they can be easily applied by working language designers. One recent paper in this direction is <i>Temporal higher-order contracts</i> by Disney, Flanagan, and McCarthy.Jeremy Siekhttps://www.blogger.com/profile/13773635290126992920noreply@blogger.comtag:blogger.com,1999:blog-11162230.post-29738612962907763192012-07-16T00:53:43.363-07:002012-07-16T00:53:43.363-07:00Nice post! What you're really after, I think, ...Nice post! What you're really after, I think, is a notion of "test": programs can then be distinguished semantically by asking whether they pass some test. A test is a context paired with a value that is expected when a program is plugged into the context and run. This is common in, e.g., pi calculi, where may-testing semantics is defined in terms of whether a program, when run in parallel with a "testing environment," outputs on a particular channel. It should be possible to adapt this notion for lambda calculi.Avik Chaudhurihttps://www.blogger.com/profile/01994850470869526814noreply@blogger.com