-
arXiv:0908.0494 [pdf, ps, other]
A Formalization of the Semantics of Functional-Logic Programming in Isabelle
Abstract: Modern functional-logic programming languages like Toy or Curry feature non-strict non-deterministic functions that behave under call-time choice semantics. A standard formulation for this semantics is the CRWL logic, that specifies a proof calculus for computing the set of possible results for each expression. In this paper we present a formalization of that calculus in the Isabelle/HOL proof a… ▽ More
Submitted 4 August, 2009; originally announced August 2009.
Journal ref: 22nd International Conference Theorem Proving for Higher-Order Logics (TPHOLs 2009): emerging trends session (2009)