Substructural Operational Semantics as Ordered Logic Programming

By Frank Pfenning and Robert J. Simmons, published in LICS 2009

This directory contains examples from the paper Substructural Operational Semantics as Ordered Logic Programming by Frank Pfenning and Robert J. Simmons, available here.

Figures from paper

Each of the figures from the paper are presented, along with illustrative examples.

• Figure 3: Call-by-value functions
• Figure 4: Mutable storage
• Figure 5: Parallel evaluation for pairs
• Figure 6: Asynchronous communication
• Figure 7: Call-by-name functions
• Figure 8: Call-by-name with destinations for binding
• Figure 9: Call-by-need functions
• Figure 10: Exceptions

Other examples

The discussion of call-by-need talkes about the black hole. An example of this appearing when the suspensions used in the call-by-need specification are straightforwardly extended to a fixed point operator, as in cbneed-fix.olf. Two ways of dealing with the stuckness that results are raising an exception or nontermination.

The discussion of exceptions includes a comment that "Exceptions entail a certain violation of modularity if the language specification requires latent propositions waiting on more than one result, as, for example, in parallel evaluation of pairs." This problem is illustrated in par-exn1.olf, and one possible solution is discussed in par-exn2.olf.