Formalizing Deterministic Semantics of DeclarativeProgramming LanguagesHeinz

Although every implementation of a (functional) logic programming language is deterministic, the languages' semantics are almost always formalized as a \nondeterministic" binary relation. Hence, there still exists a gap between the semantics of a (functional) logic programming language and its implementation which has to be closed in particular if the correctness of the implementation is to be veriied. For closing this gap we introduce a calculus in which almost every nondeterministic semantics of a (functional) logic programming language can be formalized in a unique way. The main advantage of this calculus is the straightforward implication of the deterministic semantics from the nondeterministic one.