Operational Semantics of Constraint Logic Programs with Coroutining

The semantics of constraint logic programming languages with coroutining facilities (\freeze," suspension, residuation, etc.) cannot be fully declarative; thus, an operational semantics has to be taken as the de ning one. We give a formal operational semantics for a Prolog-like language with cut and entailment-based conditional. The di culty here is to present the semantics in a form that abstracts away inessential details and highlights the interaction between language constructs. Our approach is derived from those used urrent calculi. We use abstract syntax trees, congruence laws and rewrite rules to de ne the semantics. A computation step is modeled as the ion of a rewrite rule to an abstract syntax tree modulo structural congruence. This semantics serves as a de ning tool for the language designer and as the interface between the language designer and implementor; it allows the programmer to check his intuition with a formal execution model and it gives him a performance meas...

• Type: Conference
• Year: 1995
• Where: ICLP
• Authors: Andreas Podelski, Gert Smolka
• Keywords: Abstract Syntax Tree, Automated Reasoning, ICLP 1995, Operational Semantics, Semantics