Pith. sign in

REVIEW 4 major objections 5 minor 3 cited by

Moded Types for Grassroots Logic Programs, by AI, for AI (Full Version)

T0 review · 4 major / 5 minor · reviewed 2026-08-03 · deepseek-v4-flash

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

Pith's one-line read Moded types give Grassroots Logic Programs a formal communication contract: well-typed programs produce only values conforming to declared types, even in partial runs.

desk verdict Theorem 6.5, the paper's central result, is false as stated: the moded-atom semantics contains only root-↑ terms, so contravariance is vacuously unsatisfiable for any type with input paths—the paper's own merge example fails Condition 2. read the letter →

arxiv 2601.17957 v5 pith:D75M5TPV submitted 2026-01-25 cs.PL cs.DCcs.FLcs.LOcs.MA

Ehud Shapiro This is my paper
classification cs.PLcs.DCcs.FLcs.LOcs.MA MSC 68N1703B70
keywords modedtypesgrassrootslogicprogramsconcurrentprogrammingreader/writerpairstypesoundnesspathsemanticssubtypingparameterized
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

The paper develops a type system for Grassroots Logic Programs (GLP), a concurrent logic language where every variable pair has exactly one writer and one reader. Its central claim is a soundness theorem: a program well-typed under the paper's syntactic rules will, in every run, produce only values whose 'moded paths' conform to the declared types, including runs that deadlock, fail, or never terminate. Types are regular sets of moded paths, with modes marking each subterm as consumed from or produced to the environment, and a complementation operator relates producer and consumer views. The paper also proves an 'iff' characterization: well-typing is equivalent to covariance (every output path conforms to the type) plus contravariance (every declared input path is handled by some clause). The motivation is practical: typed GLP is designed as a formal contract between a human designer and an AI code generator, letting the AI's output be checked against a precise communication specification before it runs.

What carries the argument

The moded-atom semantics: moded terms annotate each subterm with a consume (↓) or produce (↑) mode, and moded paths are the labelled paths through these terms. A GLP type is a regular set of such paths recognized by a deterministic automaton. The consistency relation compares term paths against type paths, with wildcards and primitive types at the leaves. Well-typing requires each clause head and body goal to be well-typed, every variable pair to have dual or matching types (with subtyping relaxing body-body pairs), and every input type path to be accepted by some clause. Duality, written (·)?, swaps modes and replaces each variable by its paired reader or writer, which is what lets one type

What would settle it

Construct a well-typed GLP program with a hollow stream, such as the bounded-buffer example, and run it with inputs that drive the writer mgu to bind a writer to a term containing a reader at a produced position. If the resulting moded-atoms outcome contains an output path not consistent with the declared type, the covariance direction of Theorem 6.5 is false. Concretely, modify the bounded-buffer program so the consumer fills a hollow slot with a value whose type is not the declared Integer, then type-check and run it under Definition 5.7.

Watch

Extended reading notes

Core claim

Theorem 6.5 states that a typed GLP program is well-typed if and only if (1) every output path in its moded-atom semantics is consistent with some path in the declared type (covariance), and (2) every input path in the declared type is consistent with some path in the semantics (contravariance). In particular, the soundness direction means every assignment produced by a writer in any run conforms to the declared output type. This extends typing beyond successful, total computations to partial ones, so the guarantee covers interactive protocols where communication direction can invert through hollow messages and other modal patterns.

Load-bearing premise

The proof that output conformance is preserved under reduction assumes that substituting well-typed terms into a clause keeps every position well-typed; that substitution lemma is asserted but not proved, and it is non-obvious because modes are attached to positions and a reader may sit at a position the program is supposed to produce.

Editorial extensions

If this is right

  • If Theorem 6.5 holds, a well-typed GLP program gives a runtime-independent guarantee: all output paths in any run are within the declared type, so communication contracts are enforced by construction rather than by debugging.
  • Input coverage means the program accepts every input its type promises, so a designer can rely on the type declaration as a complete interface specification.
  • Subtyping lets a client that produces a subset of a monitor's accepted operations be safely connected, extending composability beyond exact duals.
  • Parameterized types restore precision lost by monomorphic streams, so generic utilities like merge preserve element types across calls.
  • Together with the module system, these imply separately developed modules can be type-checked independently and safely linked, in either static or dynamic mode.

Reading between the lines

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

  • The soundness theorem's covariance direction depends on an unproved substitution lemma: applying a writer mgu to a well-typed clause is asserted to preserve well-typing, but the proof does not establish this for the tricky case where a reader sits at a produced position. If that lemma fails, the theorem may need a strengthened clause condition rather than the current declaration check.
  • The moded-path formulation invites a direct comparison with session types: duality and subtyping here mirror input/output variance in session types, and the deterministic type automaton could make protocol equivalence decidable in a way that process-calculus bisimulation sometimes is not.
  • A testable extension: instrument a GLP runtime to emit moded-atoms outcomes from real runs and compare them against the type automaton; any mismatch for a well-typed program would pinpoint exactly where substitution-preservation breaks.
  • Parameterized types are treated as syntactic sugar expanded before type checking; making them first-class families could be necessary for higher-order communication modalities where type parameters themselves carry mode structure.
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 / 5 minor

Summary. The paper introduces Typed GLP, a type system for Grassroots Logic Programs (GLP), a single-reader/single-writer concurrent logic language. Types are regular sets of moded paths over a moded-atom semantics that includes partial computations. A program is well-typed if clause heads/bodies conform to declared moded types and every input path is accepted by some clause. Theorem 6.5 claims that this syntactic well-typing is equivalent to a semantic characterization: covariance of output paths and contravariance of input paths between the moded-atom semantics and the type declarations. The paper also presents subtyping, a module system, parameterized types, and reports an implementation in Dart generated by AI.

Significance. If the characterization could be made correct, it would provide a formal contract for a concurrent logic language with directional communication, extending Frühwirth et al.'s LP types to interactive partial behavior, including deadlocking and nonterminating runs. The moded-atom semantics and the worked examples (merge, monitors, channels, difference lists) are suggestive and useful. The paper also delivers a concrete implementation and detailed type automata, which are valuable for reproducibility. However, the central theorem currently rests on internally inconsistent definitions and on asserted rather than proved substitution claims; the significance is therefore conditional on a substantial revision. No machine-checked proofs are provided, so the theorem and its corollaries are the main artifact to be verified.

major comments (4)
  1. [Definitions 6.1, 6.3; Theorem 6.5] As written, Condition 2 (contravariance) is false for any type with a root-↓ input path. Definition 6.1 defines input_paths(S) as paths with root mode ↓, while Definition 6.3 makes every moded-atoms outcome a produced moded term (root mode ↑; cf. Remark 5.1, 'mode ↑ throughout'). Hence the moded-atom semantics contains no input paths at all. Consistency (Definition 5.3) requires identical modes at position 0, so a root-↓ type path cannot be consistent with any root-↑ semantic path. The paper's own well-typed merge program (Example 5.3) has type path (0,↓) --> merge/3 --(1,↓)--> Stream?, so Condition 2 fails for a program the paper declares well-typed. The (⇒) proof appeals to 'the initial goal's input term paths', contradicting Definition 6.1. The authors must either redefine input paths in terms of argument positions or subpaths, or extend the semantics to include consumed moded terms.
  2. [Theorem 6.5 (⇒), Reduce paragraph] The step 'Applying σ̂ substitutes well-typed terms for variables, preserving well-typing' is asserted, not proved. It is nontrivial because modes are position-sensitive: a term substituted from a head writer position to a body reader position must be well-typed at the destination position, and head-head variable pairs (dual types) and head-body pairs (same type) behave differently. A substitution lemma establishing this is absent. Without it, the covariance half and Corollary 6.7 are unsupported. The adjacent Communicate case asserts 'Output paths are unchanged', but readers can occur at produced positions (e.g., Appendix C.3, clause 4, read(N?)), so substituting such a reader can create an output path. This needs a precise argument, not an assertion.
  3. [Theorem 6.5 (⇒), Contravariance] The contravariance proof is only a sketch. It asserts that for an input type path q one can 'construct a well-typed initial goal G0 that matches H at the input positions', but no construction is given, and no proof is provided that the resulting moded-atoms outcome contains an input path consistent with q. Under Definition 6.3 the outcome contains only produced moded terms, so the appeal to 'the initial goal's input term paths' relies on an unstated, different notion of input path. This direction needs either a rigorous construction or a redefinition of the semantics/input-path notion.
  4. [Theorem 6.5 (⇐)] The reverse direction is also a sketch. For a violation of output conformance or variable compatibility, the proof says a well-typed initial goal 'triggers' the clause and produces a bad output path, but no construction is given. In particular, a violation of Definition 5.7(3) (variable-pair type compatibility) need not manifest as any single path inconsistency; this requires a careful case analysis that is absent. The input-coverage argument assumes that 'input term paths in the moded-atoms outcome arise from the initial goal', which is exactly the contested notion from Definition 6.1. A complete proof must be supplied for this direction as well.
minor comments (5)
  1. [Conclusion] The conclusion refers to 'Theorem 6.7' where the statement appears as Corollary 6.7.
  2. [Definition 6.1] The first paragraph defines input/output paths by root mode, but the second paragraph defines them for procedure types by consumed/produced argument positions. These two notions are different and should be reconciled; the inconsistency is at the heart of Theorem 6.5.
  3. [Appendix C.9] The displayed moded-atoms outcomes do not annotate root modes (e.g., 'copy(↓[...]' vs. '↑copy(...)'), which makes it hard to see whether initial goals are consumed or produced. Since Theorem 6.5 turns on this distinction, the notation should be explicit.
  4. [Section 7] There are unresolved reference markers 'following FCP's self.cp convention [?]' and 'activate mechanism [?]'; these should be replaced with proper citations or removed.
  5. [Remark 5.1] The remark says each body unit goal is 'a produced moded term with mode ↑ throughout', but the examples annotate nested positions with ↓. The intended meaning should be clarified, perhaps 'root mode ↑, with nested modes determined by the type'.

Circularity Check

1 steps flagged · score 6.0 of 10

Theorem 6.5's contravariance half collapses by construction: the moded-atom semantics is defined to contain only produced (↑-rooted) paths, so Condition 2 has no possible witness; the proof's 'input term paths' are definitionally impossible.

  1. other [Definitions 5.1, 6.1, 6.3, 6.4, and Theorem 6.5 (Condition 2 / proof)]
    "Definition 6.3: 'Given a GLP run of a typed GLP program P=(Cs,D) with outcome (G0 :- G, σ), let G0′ be the produced moded term corresponding to G0. The moded-atoms outcome of the run are the moded-terms Hσ for every unit goal H∈G0′.' Definition 6.1: 'input_paths(S)={p∈S|p has root mode↓}'. Definition 6.4: 'The moded-atom semantics of a typed GLP program P is the set of all moded-atoms outcomes of every run of P with a well-typed initial goal.' Theorem 6.5: 'Condition 2 (Contravariance): Every input path in D is consistent with some path in the moded-atom semantics of P.'"

    By Definition 5.1, a produced moded term has all mode annotations ↑, so every moded-atoms outcome, being built from the produced G0′, contains only ↑-rooted paths. Definition 6.1 labels only ↓-rooted paths as input paths, so the moded-atom semantics has no input paths at all. Thus Condition 2's existential witness set is empty by construction. For the paper's own well-typed merge program (Example 5.3), D contains the input path (0,↓)-->merge--(1,↓)-->Stream?, so Condition 2 is false, not merely vacuously true. The (⇒) proof nevertheless says 'the initial goal's input term paths include one consistent with q'—but a produced moded term has no ↓-rooted paths. This is a definitional collapse of the contravariance half, not an independent semantic derivation.

full rationale

There are no fitted parameters, no benchmark fitting, and no load-bearing self-citation chain: the moded-atom semantics is independently operational, and the provenance of the typing rules is not what fails. The central defect is that the paper's own definitions make the semantic contravariance condition unrealizable: produced moded terms cannot witness input paths. This is a by-construction vacuity/falsity in the main theorem, so the score is above the typical 0-2 range for independent derivations. The covariance proof also contains an unproved load-bearing assertion—'Applying σ substitutes well-typed terms for variables, preserving well-typing'—and the Communicate case asserts 'Output paths are unchanged' despite readers at produced positions (cf. the monitor example, clause 4). Those are proof gaps or correctness risks rather than circular reductions. Because the definitions are not equivalent to the theorem and no self-citation/fitted-input mechanism is invoked, the score is 6 rather than 8-10.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

Theorem 6.5 rests on: standard LP machinery taken as given; the paper's own GLP operational semantics (term-matching table, Definition 3.11); the determinism restriction on type definitions (Section 5.3/Appendix D), asserted relaxable without proof; and an unproved substitution-preservation lemma plus unproved observability claims inside the theorem's proof. No fitted parameters: this is a pure theory/design paper. No new empirical entities are introduced.

assumptions (5)
  • standard math Standard LP machinery: mgu, renaming apart, instances, and the proper-run condition of Definition 2.5 are taken as given.
    Background logic-programming definitions assumed without proof, standard for the field.
  • domain assumption GLP reduction via the term-matching table (Definition 3.11) and the reader/writer substitution model correctly capture the intended operational behavior of SRSW concurrent logic programs.
    The entire type-soundness claim is relative to this operational semantics, which is the paper's own definition of GLP (§3).
  • domain assumption Types are deterministic: alternatives must be distinguishable by their top-level functor (Section 5.3 and Appendix D).
    Needed for the one-functor-per-position correspondence in Definitions 5.10-5.11 (simple prefixes, subtyping). The paper asserts this 'could be relaxed in future work without affecting the fundamental theory' (Section 5.3) but gives no proof.
  • ad hoc to paper Substitution of well-typed terms into well-typed moded terms preserves well-typedness ('Applying ˆσ substitutes well-typed terms for variables, preserving well-typing').
    Unproved lemma inside the (⇒) proof of Theorem 6.5; the crux of covariance. The adjacent Communicate case asserts output paths are unchanged, which requires readers never to occur at produced positions — contradicted by monitor clause 4 in Appendix C.3.
  • ad hoc to paper For every input type path q there exists a well-typed initial goal realizing q whose reduction makes q visible in the moded-atoms outcome.
    The (⇐) direction of Theorem 6.5 asserts this construction but does not give it; the observability of clause-body violations in the moded-atoms outcome (which tracks only the initial goal's atoms) is not established.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Moded Types for Grassroots Logic Programs, by AI, for AI (Full Version)." pith.science (2026). https://pith.science/paper/D75M5TPV

@misc{pith2026260117957,
  author       = {Pith},
  title        = {Pith review of: Moded Types for Grassroots Logic Programs, by AI, for AI (Full Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/D75M5TPV}},
  note         = {Machine review of arXiv:2601.17957}
}
read the original abstract

Grassroots Logic Programs (GLP) is a concurrent logic programming language in which logic variables are partitioned into paired readers and writers. An assignment is produced at most once via a writer and consumed at most once via its paired reader, and may contain additional readers and/or writers. This enables the concise expression of rich multidirectional communication modalities. ``Logic Programs as Types for Logic Programs'' (LICS'91) defined types as regular sets of paths over the Herbrand atom semantics of a logic program. Here, we develop a \emph{moded-atom semantics} that extends the standard Herbrand atom semantics in two ways: (\ia)~each atom subterm carries a \emph{mode}, recording whether it is consumed from or produced to the environment; and (\ib)~partial computations, including those that deadlock, fail, or never terminate, also contribute moded atoms to the semantics. We define types to be regular sets of \emph{moded paths} over this semantics, give a syntactic definition of GLP well-typing, and prove that a well-typed program is sound: every output path in its well-typed moded-atom semantics conforms to its declared output type. A type checker for GLP was implemented \emph{by} AI (Claude) in Dart, starting from the mathematical specification of Typed GLP (this paper), deriving from it an English+pseudocode spec (written by AI), and from the spec deriving Dart code (by AI). While GLP is naturally untyped, the motivation for typing it was \emph{for} AI: tasking AI to program complex communication modalities and hoping for the best turned out to be a tenuous strategy. The discipline we developed with Typed GLP is for the human designer and AI to jointly develop formal GLP type definitions and declarations, together with informal intent of the declared procedures, and only then let AI write the GLP code.

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Volition-Guarded Multiagent Atomic Transactions: Describing People and their Machines

    cs.DC 2026-04 unverdicted novelty 7.0 of 10

    Volition-guarded multiagent atomic transactions decompose agents into person volitions plus machine state, enabling formal specs and proofs that social networks and coins/bonds are volitionally grassroots under a new ...

  2. Volition Elicitation: Operational Semantics for People and Their Machines

    cs.PL 2026-07 conditional novelty 6.0 of 10

    vGLP extends GLP so that program reductions can be guarded by a person's expressed volition, with the UI derived from the semantics and correctness proofs for soundness, liveness, and compilation.

  3. GLP: A Grassroots, Multiagent, Concurrent, Logic Programming Language for AI

    cs.PL 2026-07 conditional novelty 5.0 of 10

    GLP is a single-assignment concurrent logic language whose multiagent semantics is claimed to guarantee that any program using cold-calls yields a grassroots platform, with the proof deferred to the full paper.

Reference graph

Works this paper leans on

43 extracted references · 2 linked inside Pith · cited by 3 Pith papers

  1. [1]

    Baker and Carl Hewitt

    Henry G. Baker and Carl Hewitt. The incremental garbage collection of processes. InProceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages, pages 55–59. ACM, 1977

    1977

  2. [2]

    Manifest sharing with session types

    Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Proceedings of the ACM on Programming Languages, 1(ICFP):37:1–37:29, 2017

    2017

  3. [3]

    Statically contextu- alizing large language models with typed holes

    Andrew Blinn, Xiang Li, June Hyung Kim, and Cyrus Omar. Statically contextu- alizing large language models with typed holes. InProceedings of the ACM on Programming Languages (OOPSLA), volume 8, pages 1–29. ACM, 2024

    2024

  4. [4]

    Manning Publications, 2017

    Edwin Brady.Type-Driven Development with Idris. Manning Publications, 2017

    2017

  5. [5]

    On understanding types, data abstraction, and polymorphism.Computing Surveys, 17(4):471–523, 1985

    Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism.Computing Surveys, 17(4):471–523, 1985

    1985

  6. [6]

    Colf logic programming as infinitary proof exploration.arXiv preprint arXiv:2510.12302, 2025

    Zhibo Chen and Frank Pfenning. Colf logic programming as infinitary proof exploration.arXiv preprint arXiv:2510.12302, 2025

    arXiv 2025

  7. [7]

    Parlog: parallel programming in logic.ACM Transactions on Programming Languages and Systems (TOPLAS), 8(1):1–49, 1986

    Keith Clark and Steve Gregory. Parlog: parallel programming in logic.ACM Transactions on Programming Languages and Systems (TOPLAS), 8(1):1–49, 1986

    1986

  8. [8]

    Saumya K. Debray. QD-Janus: A sequential implementation of Janus in Prolog. Software: Practice and Experience, 23(12):1337–1360, 1993

    1993

Show all 43 references
  1. [9]

    Understanding spec-driven-development: Kiro, spec-kit, and tessl.MartinFowler.com, October 2025

    Martin Fowler. Understanding spec-driven-development: Kiro, spec-kit, and tessl.MartinFowler.com, October 2025. Analyzes the shift toward using formal specifications and types as the primary interface for AI code generation

    2025

  2. [10]

    Friedman and David S

    Daniel P. Friedman and David S. Wise. The impact of applicative programming on multiprocessing.Indiana University Computer Science Department Technical Report, (TR-26), 1976

    1976

  3. [11]

    Vardi, and Eyal Yardeni

    Thom Frühwirth, Ehud Shapiro, Moshe Y. Vardi, and Eyal Yardeni. Logic pro- grams as types for logic programs. InProceedings of the 6th Annual IEEE Sympo- sium on Logic in Computer Science (LICS), pages 300–309. IEEE Computer Society, 1991

    1991

  4. [12]

    Fully abstract compositional semantics for logic programs

    Haim Gaifman and Ehud Shapiro. Fully abstract compositional semantics for logic programs. InProceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 134–142, 1989

    1989

  5. [13]

    Subtyping for session types in the pi calculus

    Simon Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2–3):191–225, 2005

    2005

  6. [14]

    Linear logic.Theoretical Computer Science, 50(1):1–101, 1987

    Jean-Yves Girard. Linear logic.Theoretical Computer Science, 50(1):1–101, 1987

    1987

  7. [15]

    Dart programming language

    Google. Dart programming language. https://dart.dev, 2024

    2024

  8. [16]

    Types for dyadic interaction

    Kohei Honda. Types for dyadic interaction. InProceedings of the 4th International Conference on Concurrency Theory (CONCUR), volume 715 ofLecture Notes in Computer Science, pages 509–523. Springer, 1993

    1993

  9. [17]

    Donald E. Knuth. Literate programming.The Computer Journal, 27(2):97–111, 1984. 16 Types for Grassroots Logic Programs

    1984

  10. [18]

    Interaction nets

    Yves Lafont. Interaction nets. InConference Record of the 17th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL), pages 95–

  11. [19]

    The semantics of the read-only variable

    Giorgio Levi and Catuscia Palamidessi. The semantics of the read-only variable. InProc. Symposium on Logic Programming, pages 128–137. IEEE, 1985

    1985

  12. [20]

    Prentice Hall, 2nd edition,

    Bertrand Meyer.Object-Oriented Software Construction. Prentice Hall, 2nd edition,

  13. [21]

    Mierowsky, S

    C. Mierowsky, S. Taylor, E. Shapiro, J. Levy, and M. Safra. On the implemen- tation of flat concurrent prolog.Proceedings of the 1985 Symposium on Logic Programming, pages 276–286, 1985

    1985

  14. [22]

    Cambridge University Press, 1999

    Robin Milner.Communicating and Mobile Systems: The 𝜋 -Calculus. Cambridge University Press, 1999

    1999

  15. [23]

    Towards a theory of types in prolog

    Prateek Mishra. Towards a theory of types in prolog. InProceedings of the 1984 International Symposium on Logic Programming, pages 289–298. IEEE, 1984

    1984

  16. [24]

    Type-constrained code generation with language models

    Niels Mündler, Rachid Guerraoui, and Martin Vechev. Type-constrained code generation with language models. InProceedings of the 46th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM,

  17. [25]

    Alan Mycroft and Richard A. O’Keefe. A polymorphic type system for Prolog. Artificial Intelligence, 23(3):295–307, 1984

    1984

  18. [26]

    Pierce.Types and Programming Languages

    Benjamin C. Pierce.Types and Programming Languages. MIT Press, 2002

    2002

  19. [27]

    Saraswat, Kenneth M

    Vijay A. Saraswat, Kenneth M. Kahn, and Jacob Levy. Janus: A step towards distributed constraint programming. InProceedings of the 1990 North American Conference on Logic Programming (NACLP), pages 431–446. MIT Press, 1990

    1990

  20. [28]

    A subset of concurrent prolog and its interpreter.ICOT Technical Report, TR-003, 1983

    Ehud Shapiro. A subset of concurrent prolog and its interpreter.ICOT Technical Report, TR-003, 1983

    1983

  21. [29]

    The family of concurrent logic programming languages.ACM Computing Surveys (CSUR), 21(3):413–510, 1989

    Ehud Shapiro. The family of concurrent logic programming languages.ACM Computing Surveys (CSUR), 21(3):413–510, 1989

    1989

  22. [30]

    Grassroots distributed systems: Concept, examples, implementa- tion and applications (brief announcement)

    Ehud Shapiro. Grassroots distributed systems: Concept, examples, implementa- tion and applications (brief announcement). In37th International Symposium on Distributed Computing (DISC 2023). (Extended version: arXiv:2301.04391), pages 47:1, 47:7, Italy, 2023. LIPICS

    2023

  23. [31]

    Glp: A grassroots, multiagent, concurrent, logic programming language.arXiv preprint arXiv:2510.15747, 2025

    Ehud Shapiro. Glp: A grassroots, multiagent, concurrent, logic programming language.arXiv preprint arXiv:2510.15747, 2025

    2025 arXiv

  24. [32]

    Grassroots platforms with atomic transactions: Social graphs, cryptocurrencies, and democratic federations

    Ehud Shapiro. Grassroots platforms with atomic transactions: Social graphs, cryptocurrencies, and democratic federations. InProceedings of the 27th Interna- tional Conference on Distributed Computing and Networking, pages 71–81, 2026. arXiv preprint arXiv:2502.11299

    2026

  25. [33]

    The execution algo- rithm of mercury: An efficient purely declarative logic programming language

    Zoltan Somogyi, Fergus Henderson, and Thomas Conway. The execution algo- rithm of mercury: An efficient purely declarative logic programming language. Journal of Logic Programming, 29(1–3):17–64, 1996

    1996

  26. [34]

    The deevolution of concurrent logic programming languages.The Journal of Logic Programming, 23(2):89–123, 1995

    Evan Tick. The deevolution of concurrent logic programming languages.The Journal of Logic Programming, 23(2):89–123, 1995

    1995

  27. [35]

    Guarded horn clauses

    Kazunori Ueda. Guarded horn clauses. InLogic Programming ’85, volume 221 of Lecture Notes in Computer Science, pages 168–179. Springer, 1986

    1986

  28. [36]

    Moded flat ghc and its message-oriented implementation tech- nique.New Generation Computing, 12(4):337–368, 1994

    Kazunori Ueda. Moded flat ghc and its message-oriented implementation tech- nique.New Generation Computing, 12(4):337–368, 1994

    1994

  29. [37]

    Resource-passing concurrent programming.Proceedings of TACS 2001, pages 95–126, 2001

    Kazunori Ueda. Resource-passing concurrent programming.Proceedings of TACS 2001, pages 95–126, 2001

    2001

  30. [38]

    I/o mode analysis in concurrent logic pro- gramming

    Kazunori Ueda and Masao Morita. I/o mode analysis in concurrent logic pro- gramming. InProceedings of the International Symposium on Theory and Practice of Parallel Programming, pages 356–368. Springer, 1995

    1995

  31. [39]

    Propositions as sessions

    Philip Wadler. Propositions as sessions. InProceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 273–286. ACM, 2012

    2012

  32. [40]

    Polymorphically typed logic pro- grams

    E YARDENI, T FRUEHWIRTH, and E SHAPIRO. Polymorphically typed logic pro- grams. InLogic Programming: Proceedings of the Eighth International Conference, pages 379–393. MIT Press, 1991

    1991

  33. [41]

    "/2 1: X 2: Xs 2: Ys 3:

    Eyal Yardeni and Ehud Shapiro. A type system for logic programs.Journal of Logic Programming, 10(2):125–153, 1991. A Deferred Proofs This appendix contains proofs of propositions from Sections 2 and 3. Proposition(2.6, LP Computation is Deduction).The outcome (𝐺0 :-𝐺𝑛)𝜎 of a p...

    1991

  34. [1997]

    Introduces Design by Contract

  35. [2025]

    Available at https://arxiv.org/abs/2504.09246

    arXiv

Pith tools

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