Pith. sign in

REVIEW 4 major objections 3 minor 28 references

An Execution Model for RICE

T0 review · 4 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper gives RICE's execution model and proves it agrees with Curry's standard semantics on terminating first-order programs.

desk verdict A useful operational model for RICE's backtracking execution, but the advertised conformance statement is only soundness for a first-order fragment, not the completeness the conclusion claims. read the letter →

arxiv 2506.05839 v1 pith:ZVVA6Z6J submitted 2025-06-06 cs.PL

Steven Libby This is my paper
classification cs.PL
keywords operationalsemanticsCurryFlatbacktrackingnarrowingfunctionallogicprogrammingexecutionmodelRICEcompiler
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper gives an execution model for RICE, a Curry compiler that resolves non-determinism by backtracking. The model is presented as an operational semantics over a heap graph, with forwarding nodes that preserve sharing and a stack that records every rewrite so evaluation can be undone when backtracking. The paper's central claim is a conformance theorem: for terminating programs, evaluation in this model eventually produces exactly the values that the standard natural semantics for Curry produces. That matters because a precise execution model turns an optimizing C backend into a target one can reason about and verify.

What carries the argument

The machinery is a graph of heap nodes (failure, free, choice, constructor, function, forwarding, and partial-application nodes) together with a backtracking stack of rewrite frames. Evaluation is defined by three relations: normalization to a value, head normalization, and backtracking; the case and apply rules are where non-determinism is resolved. The forwarding node *(g) preserves sharing when a function returns one of its parameters, so backtracking can undo rewrites without duplicating subgraphs.

What would settle it

Run the execution model on a terminating higher-order expression such as (id ? not) True and check that the apply and choice rules enumerate both True and False as the standard Curry semantics does; because the conformance proof only covers first-order expressions, any mismatch in the answers, or any divergence, refutes the paper's unrestricted final claim.

Watch

Extended reading notes

Core claim

The discovery is that a deterministic backtracking semantics can faithfully implement Curry's nondeterministic natural semantics. Theorem 1 shows that any graph-changing evaluation can be undone by backtracking steps, restoring the original graph up to unreachable bindings. Theorem 2 shows that for first-order expressions with all applications fully applied, every derivation in the new semantics maps to a derivation in the standard natural semantics, with forwarding nodes contracted. The intended upshot, stated as the paper's final claim, is that if a terminating expression evaluates to a value under the standard semantics, it will eventually evaluate to that same value under RICE's semantics.

Load-bearing premise

The conformance proof assumes every expression is first-order and every application is fully applied, yet the paper's final claim drops that restriction; if higher-order or partially applied programs behave differently under the apply rules, the unrestricted claim has no support.

Editorial extensions

If this is right

  • For terminating first-order programs, RICE's evaluator and the standard Curry semantics agree on values, so the existing C code generator is justified within that scope.
  • Failure becomes an explicit bottom node that propagates until it is discarded, explaining how failed branches are dropped while backtracking.
  • Choices are kept as heap nodes and only refined when scrutinized, matching the generated code's tag-dispatch loop.
  • The backtracking stack records every graph-changing rewrite, and Theorem 1 certifies that any value can be undone to try the next alternative.
  • Higher-order code is not excluded from the model: the apply rules give a defined eval-apply behavior for partial applications, but that part has no conformance proof.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The proof's first-order restriction can likely be lifted by adding an explicit apply counterpart to the natural semantics and showing the eval-apply rules are a simulation; the mapping in the paper gives a direct recipe for that extension.
  • Because the search strategy is encoded in the semantics, the number of backtracking steps becomes a measurable quantity, opening the door to complexity bounds and to semantic comparisons of leftmost-first versus fair search.
  • The forwarding-node trick suggests that preserving sharing during backtracking is a general requirement for lazy functional logic languages, not just for RICE.
  • A natural experiment would be to compile a suite of higher-order Curry programs with RICE and compare their answers against the standard semantics; any mismatch would isolate exactly where the missing proof would need repair.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 3 minor

Summary. The paper presents an execution model for the RICE Curry compiler. It defines a restricted FlatCurry syntax organized into blocks, statements, and expressions; represents the heap as a directed graph with nodes for failure, choice, free variables, forwarding, and partial applications; and gives a deterministic operational semantics with an explicit backtracking stack. It then sketches a correspondence between the semantics and generated C code and compares the model to Albert et al.'s natural semantics for Curry. The concluding claim is that for terminating programs, any value derivable in the natural semantics is eventually produced by the RICE execution model.

Significance. The paper addresses a real need: a precise, implementation-level semantics for a Curry compiler based on backtracking rather than pull-tabbing. The graph representation, the backtracking stack, and the explicit case and apply rules in Sections 5-6 are concrete, and the example in Section 7 usefully connects the semantics to RICE's generated C code. If the correctness claim were established, this would be a valuable foundation for reasoning about RICE and its optimizations. As it stands, however, the correctness argument is incomplete: Theorem 2 establishes only a one-way soundness statement for a restricted first-order fragment, and the advertised equivalence/completeness claim in Section 8 is not proved. The paper therefore currently contributes a detailed execution model with an incomplete conformance argument.

major comments (4)
  1. [§8 (final paragraph)] The final sentence claims that if a terminating expression e evaluates to a value v in the natural semantics, then e will eventually evaluate to v in the RICE semantics. This is a completeness claim, but Theorem 2 proves the opposite implication: it shows that if the RICE semantics evaluates to a constructor or literal v, then the natural semantics can also produce v. Neither Theorem 1 nor Theorem 2 shows that every natural-semantics derivation is reachable by the left-to-right backtracking search; Theorem 1 only says that a completed evaluation can be undone, not that all answers are eventually found. The closing correctness claim is therefore unsupported by the preceding results.
  2. [§8, first paragraph and Figure 7 (Norm-Choice)] The paper admits: 'Because we are not using a fair evaluation strategy, there will be answers that we may not produce in a finite amount of time.' Together with the left-to-right commitment in (Norm-Choice), (Case-Choice), and (Apply-Choice), this directly conflicts with the final claim unless 'terminating expression' is defined to mean that every branch of the search tree terminates. Under the usual reading of 'terminating' as 'has a value in the natural semantics', an expression whose left branch diverges while a right branch yields v is a counterexample. The paper must either define the restricted class and prove that the backtracking search is complete for it, or remove the completeness claim.
  3. [§8, Theorem 2] Theorem 2 is stated for the head-normal-form relation ⇓, not for the normal-form relation ⇓N used in the paper's final correctness statement. The proof also assumes that 'all expressions are first order and all applications are fully applied', and the author notes that the natural semantics is not formulated for higher-order expressions. However, the execution model includes apply rules, PART nodes, and higher-order behavior (Figures 5 and 10), and the final claim is stated without restriction. Consequently, conformance for higher-order and partial applications, which is a substantial part of the model's novelty, is not established, and the normal-form evaluation rules such as (Norm-Con) and (Norm-Choice) are not covered by the theorem.
  4. [§8, Figure 13] The proof says 'The full mapping can be found in Figure 13', but the figure omits several rules used by the execution model: (Case-Con), (Case-ConFree), (Case-Lit), and all apply rules. The text's remarks that the missing cases are 'identical' or 'straightforward' do not supply the required derivations. Since Theorem 2 is the only result connecting the RICE semantics to the natural semantics, the correspondence argument is incomplete as written.
minor comments (3)
  1. [§2, §7, references] There are several typos and formatting slips, including 'returen' in Section 2, 'Avalible' in reference [23], and 'srutinee'/'scrutinee' in Figure 12; the URL for reference [1] also appears malformed. A copyedit would improve readability.
  2. [§5 and rules (Fun), (Case-Fun)] The graph notation is not entirely consistent: Figure 5 writes f(g) and C(g) with g a graph, while rules such as (Fun) write f(y) with y a variable; clarifying whether arguments are graph nodes or variable references would prevent confusion when reading the apply rules.
  3. [§3 and Figures 2, 9] The status of literals is unclear: Section 3 says literals and primitive operations are outside the paper's scope, yet literals appear throughout the syntax and in rules such as (Case-Lit) and (Case-LitFree), and the recalled natural semantics in Figure 2 does not include literal patterns. The paper should state exactly which fragment is being treated.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the conformance argument is anchored to the independent natural semantics of Albert et al.; self-citations are not load-bearing.

full rationale

The derivation is not circular. The execution model's rules (Figures 7–10) are defined independently and then related to the natural semantics of Albert et al. [2] via the correspondence mapping in Figure 13; the target semantics is an external, published semantics, not a re-statement of the RICE model. Self-citations to [23] support performance and implementation claims only (e.g., the choice of backtracking over pull-tabbing), and they do not carry the conformance proof. No fitted parameters, self-referential definitions, or uniqueness arguments imported from the author's prior work appear in the derivation. The one notable issue is a correctness gap, not a circular one: the final sentence of Section 8 claims 'If we have a terminating expression e, and e evaluates to a value v in the natural semantics, then it will eventually evaluate to v in our semantics,' which is a completeness statement. However, Theorem 2 proves only the soundness direction and does so under the stated restriction that 'all expressions are first order and all applications are fully applied.' The paper itself concedes earlier in Section 8 that 'there will be answers that we may not produce in a finite amount of time,' and Theorem 1 only shows that backtracking can restore the earlier graph, not that every natural-semantics answer is eventually reached. This hidden scope restriction and the missing completeness proof are correctness risks, but they do not make the derivation circular: the conclusion is not assumed as a premise, it is simply not established by the stated theorems.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

No numerical fitting occurs in this semantics paper. The ledger instead captures the proof assumptions: the external natural semantics, the unproven semantics-preservation of the restrictions, the informal graph-to-heap correspondence, and the unproven completeness of the backtracking strategy.

assumptions (4)
  • domain assumption The natural semantics of Curry given by Albert et al. is the correct reference semantics.
    Used as the ground truth in Theorem 2; the paper does not formalize or prove this semantics.
  • domain assumption Restricted FlatCurry transformations (trivial arguments, one case per function, early lets) preserve Curry semantics.
    Section 4 describes restrictions without a preservation proof; Figure 3 gives only an example.
  • ad hoc to paper A graph G can be paired with a heap Gamma in the natural semantics, and forwarding nodes can be contracted without changing meanings.
    Theorem 2 relies on this correspondence but never defines it formally; this is a gap specific to this paper's proof.
  • ad hoc to paper For terminating programs, the leftmost backtracking strategy is complete.
    This is exactly the unproven converse of Theorem 2; the conclusion assumes it without derivation.
invented entities (2)
  • Forwarding node *(g)
    purpose: Preserves sharing when a function returns one of its parameters, so backtracking can restore shared subgraphs without copying.
    Introduced in Section 5 to solve the graph-copying problem for backtracking; its behavior is justified only by the paper's own conformance theorem, not by an external benchmark.
  • PART node (partial application)
    purpose: Represents partially applied functions and constructors in the heap.
    A standard eval-apply device; the paper offers no independent validation of this specific heap representation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of An Execution Model for RICE." pith.science (2026). https://pith.science/paper/ZVVA6Z6J

@misc{pith2026250605839,
  author       = {Pith},
  title        = {Pith review of: An Execution Model for RICE},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZVVA6Z6J}},
  note         = {Machine review of arXiv:2506.05839}
}
read the original abstract

In this paper, we build on the previous work of the RICE compiler by giving its execution model. We show the restrictions to the FlatCurry language that were made to produce executable code, and present the execution model using operational semantics similar to Launchbury. Finally, we show that the execution model conforms with the standard operational semantics for Curry.

Figures

Figures reproduced from arXiv: 2506.05839 by the authors.

Figure 1
Figure 1. The syntax of FlatCurry We use the convention of [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Natural semantics for Curry [2] Following the conventions, Γ[x 7→ v] can be used to lookup or update variable x in heap Γ with value v [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. A Curry function, a FlatCurry function, and a restr [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Syntax of restricted FlatCurry 5 Heap Representation Now that we have a syntax for Curry, we can discuss the execution model. A Curry program consists of a set of functions as well as a single expression to evaluate. The expression is represented as a directed rooted g…
Figure 5
Figure 5. Figure 5: Heap objects represented as a graph. and prevent any unintended copying. Our example from before evaluates to the following. xor * * ? True False 6 The Execution Model To run a Curry program, we evaluate the expression main to normal form (or a value). We can accomplis…
Figure 6
Figure 6. Figure 6: evaluation relations expression e with graph G and stack S evaluates to value v with a possibly modified G and S. (BT) G,hx,y|Si ⇓B G[x 7→ y],S (BT-Choice) G,hx,y | l?,r | Si ⇓B? G[x 7→ y][l 7→ r],hr,?(l,r)|Si (Norm-Bot) G,S : e ⇓ G1,S1 : ⊥ G,S : e ⇓N G1,S1 : ⊥ (Norm-L…
Figure 7
Figure 7. Figure 7: backtracking and normalization algorithm. [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]
Figure 8
Figure 8. Figure 8: Evaluation of expressions without case We assume all variables from function definitions are fresh. we need to create a forwarding node for the reasons described above. More substantial changes start to appear in the case rules. These rules correspond to the while/swit…
Figure 9
Figure 9. Figure 9: rules for Case expressions. In Case-LitFree SL = hx,l2|...|x,ln|x,free|S1i In Case-ConFree SC = hx,C2(free)|...|x,Cn(free)|x,free|S1i [PITH_FULL_IMAGE:figures/full_fig_p011_9.png]
Figure 10
Figure 10. Figure 10: apply rules. In all 3 rules Gx = G[x 7→ PART(f,k,y)] In (apply-over) ek = e1 ... ek In (apply-over) ek+1 = ek+1 ... en applied, then it must evaluate to a PART; we take the first few arguments, evaluate to the PART, and supply the final arguments. 7 Correspondence to …
Figure 11
Figure 11. Figure 11: Definition for a Node object void n ot _ h n f ( f i e l d r o o t ) { Node* s c r u t i n e e = r o ot −> c h i l d r e n [ 0 ] ; wh ile ( t r u e ) { switch ( s c r u t i n e e −> t a g ) { case FAIL_TAG : r o ot −> s c r u t i n e e = FAIL_symbol ; r o ot −> c h i …
Figure 12
Figure 12. Figure 12: Code for reducing a not node to head normal form [PITH_FULL_IMAGE:figures/full_fig_p013_12.png]
Figure 13
Figure 13. Figure 13: The mapping ⇔ [PITH_FULL_IMAGE:figures/full_fig_p016_13.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

28 extracted references · 25 canonical work pages

  1. [1]

    Albert, M

    E. Albert, M. Hanus, F. Huch, J. Oliver & G. Vidal (2002): A Determinis- tic Operational Semantics for Functional Logic Programs , p. 207. Available at https://www.programmazionelogica.it/wp-content/uplo ads/2002/09/agp02_207.pdf

    work page 2002

  2. [2]

    Albert, M

    E. Albert, M. Hanus, F. Huch, J. Oliver & G. Vidal (2005): Operational semantics for declarative multi- paradigm languages. Journal of Symbolic Computation 40(1), pp. 795–829, doi:10.1016/j.jsc.2004.01.001

    work page doi:10.1016/j.jsc.2004.01.001 2005

  3. [3]

    Antoy (1992): Definitional Trees

    S. Antoy (1992): Definitional Trees . In H. Kirchner & G. Levi, editors: Algebraic and Logic Program- ming, Third International Conference, V olterra, Italy, Se ptember 2-4, 1992, Proceedings , Lecture Notes in Computer Science 632, Springer, pp. 143–157, doi:10.1007/BFB0013825

    work page doi:10.1007/bfb0013825 1992

  4. [4]

    Antoy (1997): Optimal Non-deterministic Functional Logic Computations

    S. Antoy (1997): Optimal Non-deterministic Functional Logic Computations . In M. Hanus, J. Heering & K. Meinke, editors: Algebraic and Logic Programming, 6th International Joint C onference, ALP ’97 - HOA ’97, Southampton, UK, September 3-5, 1997, Proceedings , Lecture Notes in Computer Science 1298, Springer, pp. 16–30, doi:10.1007/BFB0027000

    work page doi:10.1007/bfb0027000 1997

  5. [5]

    Antoy, R

    S. Antoy, R. Echahed & M. Hanus (2000): A needed narrowing strategy . J. ACM 47(4), pp. 776–822, doi:10.1145/347476.347484

    work page arXiv 2000

  6. [6]

    Antoy, M

    S. Antoy, M. Hanus, A. Jost & S. Libby (2019): ICurry 12057, pp. 286–307. doi:10.1007/978-3-030-46714-2_18

    work page doi:10.1007/978-3-030-46714-2_18 2019

  7. [7]

    Antoy & A

    S. Antoy & A. Jost (2016): A New Functional-Logic Compiler for Curry: Sprite 10184, pp. 97–113. doi:10.1007/978-3-319-63139-4_6

    work page doi:10.1007/978-3-319-63139-4_6 2016

  8. [8]

    A. W . Appel (2006): Compiling with Continuations (corr . version). Cambridge University Press

    work page 2006

Show all 28 references
  1. [9]

    Augustsson, J

    L. Augustsson, J. Breitner, K. Claessen, R. Jhala, S. Pey ton Jones, O. Shivers, G. L. Steele Jr. & T. Sweeney (2023): The V erse Calculus: A Core Calculus for Deterministic Functional Logic Programming. Proceedings of the ACM on Programming Languages 7(ICFP), pp. 417–447, doi...

    2023 doi

  2. [10]

    J. Böhm, M. Hanus & F. Teegen (2021): From Non-determinism to Goroutines: A Fair Implementation of Curry in Go . In N.ò V eltri, N. Benton & S. Ghilezan, editors: PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, Tal linn, Estonia, ...

    2021

  3. [11]

    Braßel (2010): Implementing Functional Logic Programs by Translation int o Purely Functional Programs

    B. Braßel (2010): Implementing Functional Logic Programs by Translation int o Purely Functional Programs . Ph.D. thesis, University of Kiel. Available at http://eldiss.uni-kiel.de/macau/receive/dissertatio n_diss_00007056

    2010

  4. [12]

    Braßel, M

    B. Braßel, M. Hanus, B. Peemöller & F. Reck (2011): KiCS2: A New Compiler from Curry to Haskell . In: H. Kuchen, editor: Functional and Constraint Logic Programming, 20th Interna tional Workshop, WFLP 2011, Odense, Denmark, July 19, 2011, Proceedings , Lecture Notes in Compute...

    2011 doi

  5. [13]

    Echahed & J

    R. Echahed & J. C. Janodet (1997): On constructor-based graph rewriting systems . Technical Report 985-I, IMAG. Available at ftp://ftp.imag.fr/pub/labo-LEIBNIZ/ OLD-archives/PMP/c-graph-rewriting.ps.gz

    1997

  6. [14]

    Hanus (ed.) (March 04, 2017): PAKCS 1.14.3: The Portland Aachen Kiel Curry System

    M. Hanus (ed.) (March 04, 2017): PAKCS 1.14.3: The Portland Aachen Kiel Curry System . Available at http://www.informatik.uni-kiel.de/~pakcs

    2017

  7. [15]

    Flanagan, A

    C. Flanagan, A. Sabry, B. F. Duba & M. Felleisen (1993): The Essence of Compiling with Continuations . In R. Cartwright, editor: Proceedings of the ACM SIGPLAN’93 Conference on Programmin g Language Design and Implementation (PLDI), Albuquerque, New Mexico , USA, June 23-25, 1...

    1993

  8. [16]

    Hanus (2013): Functional Logic Programming: From Theory to Curry , pp

    M. Hanus (2013): Functional Logic Programming: From Theory to Curry , pp. 123–168. Lecture Notes in Computer Science 7797, Springer, doi:10.1007/978-3-642-37651-1_6

    2013 doi

  9. [17]

    Hußmann (1988): Nondeterministic Algebraic Specifications and Nonconfluen t T erm Rewriting

    H. Hußmann (1988): Nondeterministic Algebraic Specifications and Nonconfluen t T erm Rewriting . In J. Grabowski, P . Lescanne & W . Wechler, editors: Algebraic and Logic Programming, International Work- S. Libby 129 shop, Gaussig, GDR, November 14-18, 1988, Proceedings , Lectur...

    1988 doi

  10. [18]

    Johnsson (1985): Lambda Lifting: Treansforming Programs to Recursive Equat ions

    T. Johnsson (1985): Lambda Lifting: Treansforming Programs to Recursive Equat ions. In J. Jouan- naud, editor: Functional Programming Languages and Computer Architectu re, FPCA 1985, Nancy, France, September 16-19, 1985, Proceedings , Lecture Notes in Computer Science 201, Spr...

    1985 doi

  11. [19]

    S. L. Peyton Jones (1987): The Implementation of Functional Programming Languages . Prentice-Hall, Inc., Upper Saddle River, NJ, USA

    1987

  12. [20]

    S. L. Peyton Jones & J. Salkild (1989): The Spineless T agless G-Machine. In J. E. Stoy, editor: Proceedings of the fourth international conference on Functional program ming languages and computer architecture, FPCA 1989, London, UK, September 11-13, 1989 , ACM, pp. 184–201, ...

    1989

  13. [21]

    Launchbury (1993): A Natural Semantics for Lazy Evaluation

    J. Launchbury (1993): A Natural Semantics for Lazy Evaluation . In: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’93, Association for Com- puting Machinery, New Y ork, NY , USA, p. 144–154, doi:10.1145/158511.158618

    1993

  14. [22]

    Libby (2023): RICE: An Optimizing Curry Compiler

    S. Libby (2023): RICE: An Optimizing Curry Compiler . In M. Hanus & D. Inclezan, editors: Prac- tical Aspects of Declarative Languages - 25th Internationa l Symposium, P ADL 2023, Boston, MA, USA, January 16-17, 2023, Proceedings , Lecture Notes in Computer Science 13880, Spri...

    2023 doi

  15. [23]

    Libby (June 21, 2022): Making Curry with Rice: An Optimizing Curry Compiler

    S. Libby (June 21, 2022): Making Curry with Rice: An Optimizing Curry Compiler . Ph.D. thesis, Portland State University, doi:10.15760/etd.7964. Avalible at htt ps://github.com/slibby05/rice

    2022 doi

  16. [24]

    W . Lux & H. Kuchen (1999): An Efficient Abstract Machine for Curry . In K. Beiersdörfer, G. En- gels & W . Schäfer, editors: Informatik ’99 - Informatik überwindet Grenzen, 29. Jahres tagung der Gesellschaft für Informatik, Paderborn, 5.-9. Oktober 199 9, Informatik Aktuell, S...

    1999 doi

  17. [25]

    Marlow & S

    S. Marlow & S. L. Peyton Jones (2004): Making a fast curry: push/enter vs. eval/apply for higher-o rder languages. In C. Okasaki & K. Fisher, editors: Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird , UT, USA, Septe...

    2004

  18. [26]

    Mayr & T

    R. Mayr & T. Nipkow (1998): Higher-Order Rewrite Systems and Their Confluence . Theoretical Computer Science 192(1), pp. 3–29, doi:10.1016/S0304-3975(97)00143-6

    1998 doi

  19. [27]

    Mehner, D

    S. Mehner, D. Seidel, L. Straßburger & J. V oigtländer (2 014): Parametricity and Proving Free Theorems for Functional-Logic Languages. In O. Chitil, A. King & O. Danvy, editors: Proceedings of the 16th International Symposium on Principles and Practice of Declarative Progra m...

    2014

  20. [28]

    J. C. González Moreno, M. T. Hortalá-González, F. J. Lóp ez-Fraguas & M. Rodríguez-Artalejo (1996): A Rewriting Logic for Declarative Programming . In H. R. Nielson, editor: Programming Languages and Sys- tems - ESOP’96, 6th European Symposium on Programming, Link öping, Swede...

    1996 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.