Pith. sign in

REVIEW 4 major objections 5 minor 26 references

Compiling to recurrent neurons

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 ↗ Review JSON

Pith's one-line read A typed language with loops compiles exactly into the dynamics of linear recurrent neurons.

desk verdict The metatheory for compiling iteration to recurrent neurons is a real and incremental advance; the experiments are a useful prototype, but they do not test the theorem's scope. read the letter →

arxiv 2511.14953 v2 pith:EW2ZN6X5 submitted 2025-11-18 cs.PL cs.LG

Joey Velez-Ginorio , Nada Amin , Konrad Kording , Steve Zdancewic This is my paper · ORCID
classification cs.PLcs.LG
keywords differentiableprogramminglinearrecurrentneuronsiterationtypescompilercorrectnessdenotationalsemanticsprimitiverecursionneurosymbolic
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

Iteration does not have to be banned from differentiable programs. The paper presents Cajal(⊸,2,N), a minimal typed higher-order linear language with an iterator, and proves a compiler-correctness theorem: for closed programs of boolean or natural-number type, the compiled multilinear map of a program coincides with the compiled map of its evaluated value and is distinct from the compiled map of every other value. The compiler turns iteration into a linear combination of the states of a discrete-time linear dynamical system—a recurrent neuron—so the loop becomes a differentiable linear map. In two image-transformation experiments, wiring such compiled loops into a neural network leads to faster learning and greater data-efficiency than a network without first-class iteration. If the proof's scope extends to the open, real-valued programs used in training, ordinary discrete programming structures become available inside gradient-based learning.

What carries the argument

The load-bearing object is the compiler from typing derivations to multilinear maps, whose iteration clause is the linear combination sum_{n in N} ⟦e3⟧(n) * (⟦e2⟧)^n (⟦e1⟧). This is precisely a discrete-time linear dynamical system: a one-hot vector in time selects the state at step n, the iterated step map applies the loop body n times, and the sum over n fuses the base case with the recurrence. Linear typing—no contraction and no weakening—is what makes every compiled judgment genuinely multilinear, and the finitely supported sequence space for N gives the infinite sum enough structure to be a well-defined linear map that becomes differentiable once truncated to a finite horizon. The compi

What would settle it

Take any closed base-type program e and its compiled map; the theorem predicts that the compiled map equals the compiled map of exactly the value e evaluates to and differs from the compiled map of every other value. A single counterexample—two distinct evaluating programs with identical compiled maps, or a compiled map equal to the compiled map of the wrong value—would settle the central claim against the paper.

Watch

Extended reading notes

Core claim

The central claim is that primitive recursion over natural numbers can be compiled to the equations of linear recurrent neurons while preserving program behavior. The compiler maps typing derivations to multilinear maps over R-vector spaces: booleans become R^2, natural numbers become finite-support sequences indexed by time, and an iterator iter{e1|y->e2}(e3) becomes the sum over n of evaluation of e3 at n multiplied by the n-th power of the step map applied to the base case. Theorem 2 states that for closed base-type programs, if e evaluates to v then the compiled map of e equals the compiled map of v, and if e does not evaluate to v then the compiled maps differ; since all well-typed clos

Load-bearing premise

The formal correctness theorem covers only closed programs over booleans and natural numbers; the training recipe assumes that the same behavior, truncated to 10 time steps, holds for open programs over reals, images, and learned linear maps.

Editorial extensions

If this is right

  • Discrete iteration can appear anywhere inside a differentiable program, including inside a neural network architecture, without breaking the gradients needed for gradient-based learning.
  • The correctness theorem gives a formal soundness-and-adequacy guarantee that the compiled recurrent dynamics faithfully implement the source loop—a guarantee the paper notes is absent from earlier neurosymbolic compilers.
  • The experiments show that first-class iteration helps a network learn an iterative image transform faster and with greater data-efficiency, and that this advantage persists even when the compiled map is replaced by a random type-preserving map.
  • The same type-theoretic recipe is a natural next step for primitive recursion over lists, trees, and algebraic data via linear recursive neurons, as the paper itself proposes in its discussion.

Reading between the lines

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

  • If the finite-truncation assumption holds, the same compilation pattern should scale to any inductive data type whose elements can be indexed in time—lists, trees, and other algebraic data—by replacing the single recurrence with a linear recursive neuron; this is an extension the paper proposes but does not prove.
  • The near-parity of the correctness-preserving model and the random type-preserving model in Experiment 1 suggests that much of the learning-speed advantage may come from the linear type-shape and the factored architecture it imposes, rather than from the specific compiler equations; one way to test this is to compare the compiled iterator with another linear map of the same multilinear arity but d
  • Because the authors observe that linked vectors of large norm destabilize training, a practical extension is to add a norm bound on linked vectors; if that removes the early instability of the correct model, it would separate the effect of compilation correctness from the effect of initialization scale.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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 Cajal(⊸,2,N), a linearly typed, higher-order language with booleans, natural numbers, and iteration, and claims to compile it to differentiable form as linear recurrent neurons. The core theoretical result (Theorem 2, §4.2) asserts that for closed programs of base type, the compiled multilinear map equals the compiled value iff the program evaluates to that value; this is presented as soundness and adequacy of a denotational semantics. The paper also reports a PyTorch implementation and two experiments on iterative image transformation, where programming the iteration explicitly yields faster and more data-efficient learning than a baseline or a random-matrix 'type-preserving' variant.

Significance. If the metatheory is completed, the paper makes a genuinely useful contribution: it identifies a class of linear programs for which iteration can be given a denotational semantics in terms of linear dynamical systems, and it proves a plausible correctness theorem for the closed base-type fragment. The design is clean, the connection to Köthe sequence spaces and prior work on conditionals is well motivated, and the experiments include an ablation (Model T) that helps attribute the benefit to structure rather than parameter count. The paper is also honest about practical limitations, explicitly flagging the finite-horizon truncation and the need to exclude vblur from Model T. However, as written, the proof appendices contain material gaps, and the theorem's scope is narrower than the abstract's claim that 'its programs compile correctly to recurrent neurons.'

major comments (4)
  1. [Theorem 2 vs. §5.1.2, §5.2.2] Theorem 2 covers only closed programs of base type 2 or N (and uses the undefined predicate 'base(τ)'). The experiments, however, compile open programs over R784, R10, and Lin(R784,R784), and truncate the iteration to a fixed horizon of 10 steps ('During training it is typical to assume a maximum number of steps'). No theorem connects the 10-step truncated map to the infinite denotation ⟦iter⟧, nor does the formal language include real-typed vectors or the particular programs displayed for Models D and T. Consequently, the empirical results do not demonstrate the formal 'compiles correctly' claim in the regime where the benefit is claimed. Either extend the metatheory to open real-typed programs with a verified finite-horizon approximation, or substantially rescope the abstract/introduction claims.
  2. [Appendix B.4, B.5, B.6] The main text says 'Appendix B.4 contains a detailed proof' of Theorem 2, but B.4 is only a restatement: it derives (a) from 'compiler preserves what programs will do' and (b) from 'compiler preserves what programs won't do', which are the lemmas being proved. The actual proofs in B.5 and B.6 are sketches and rely on unproved meta-theorems: B.5 invokes 'Because evaluation preserves typing' and 'Because closing substitutions preserve typing' without a corresponding lemma in the appendix. B.6's adequacy argument is also informal ('By negation', contradiction between one-hot vectors). For a POPL-style paper whose central contribution is a compiler correctness proof, this is a load-bearing omission.
  3. [Appendix B.9, Lemma (homogeneous maps)] The statement of the homogeneity lemma is malformed: 'Δ,𝑥 :𝜏₁⊢𝑒 :𝜏₂ =⇒ 𝛼·⟦𝑒⟧(®𝜎,®𝑥)' has no right-hand side and cannot be parsed as an equality. The intended statement is presumably '⟦𝑒⟧(®𝜎,𝛼·®𝑥) = 𝛼·⟦𝑒⟧(®𝜎,®𝑥)'. The proof is omitted ('similar to showing the compiler maps programs to additive maps'). Since Lemma 4 (multilinearity) depends on both additivity and homogeneity, this gap directly affects the proof of compiler soundness.
  4. [Appendix B.2 and Fig. 11] In the logical-relation proof of Theorem 1, the iteration case invokes 'backward closure of the logical relation' without defining this notion or proving it for RE⟦τ⟧. The case analysis is also only a sketch. Separately, Fig. 11's definition of ⟦N⟧, '{𝑥 : N→ R | ∃𝑛, supp(𝑥) = 𝑛}', is ill-formed: supp(𝑥) is a set, not a natural number. The finite-support condition is essential for the well-definedness of the infinite sums in Fig. 13, so a precise definition (e.g., 'finite support') is needed.
minor comments (5)
  1. [Theorem 2] The predicate 'base(τ)' is used but never defined. Please either define it or state the theorem in terms of types 2 and N explicitly.
  2. [§5.1.2, footnotes 8–9] The self-flagged limitations are helpful but should be discussed more prominently. The finite-horizon truncation is not just a training detail; it is a semantic deviation from the infinite-time iterator, and the paper should acknowledge that the experiments are evidence of practical utility, not a validation of the formal theorem.
  3. [Fig. 13] The notation (⟦𝑒₂⟧)ⁿ in the iterator rule is ambiguous for open contexts. Since ⟦𝑒₂⟧(σ) is a linear map after applying the environment, clarify that the power is taken on the linear map, not on the syntactic expression.
  4. [Figures 14 and 17] The prototypical learning dynamics are shown for a single seed in each figure. The PSNR summaries in Figs. 15–16 are more informative. Consider adding error bars or a statistical test across seeds to support claims like 'Model D and Model T learn comparably well' and 'Model D now exhibits the best PSNR.'
  5. [Appendix B.1] The main text says Appendix B.1 contains a detailed proof of Theorem 1, but it is a five-line argument that restates the logical-relation facts. Either expand it or retitle it as a proof outline.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation: the compiler correctness theorem is proved by induction in a self-contained calculus; the main gap is that the experiments use open, real-typed programs and a 10-step truncation not covered by Theorem 2, which is an applicability limitation, not a circularity.

full rationale

The paper's load-bearing claim is Theorem 2, proved in Appendix B by induction on the evaluation relation and on the structure of the compiler in Fig. 13. The denotation of iteration, ⟦iter{...}⟧ = Σ_n ⟦e3⟧(n)·(⟦e2⟧)^n(⟦e1⟧), is a definition of the compiler, and correctness consists in showing it agrees with the independently specified big-step evaluation relation of Fig. 8; this is a genuine soundness/adequacy argument rather than a reduction of the conclusion to the premise. No parameter is fitted and then renamed as a prediction. The paper does cite the same authors' prior work [20] (and co-authored [19]) for the prior status of conditionals and for inspiration, but the iteration theorem does not import its content from those citations; the proof is self-contained. The self-flagged limitations — 'During training it is typical to assume a maximum number of steps' (Section 5.1.2) and 'The exclusion of vblur is necessary, otherwise the dimensionality explodes' (Section 5.1.2), plus the use of open programs with types R784 and Lin(R784,R784) that are absent from Fig. 7 — mean the experiments are not fully covered by Theorem 2. That is a correctness/external-validity gap, not circularity, because the experimental regime is not used to define or justify the theorem. Score 2 reflects only the presence of non-load-bearing self-citation.

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

The central theoretical result rests on standard PL meta-theory (subject reduction, exchange, Barendregt) plus the finitely-supported-sequence semantics for N. The main load-bearing domain assumption is finite support and the practical truncation to K=10 steps. No fitted parameters appear in the formal system; the only hand-chosen constant is the horizon K=10 in the experiments.

free parameters (1)
  • maximum unrolling horizon K = 10
    Experiments truncate the infinite-time recurrence to 10 steps (Section 5.1.2, 'assume a maximum number of steps'); chosen because digits are 0–9. This turns the infinite-dimensional compiled map into a finite-dimensional differentiable program, but is not derived from the correctness theorem.
assumptions (5)
  • domain assumption Evaluation preserves typing, and closing substitutions preserve typing.
    Used repeatedly in Appendix B.5 in the proof of Lemma 3 (e.g., 'Because evaluation preserves typing'), but no proof or reference is given in the paper.
  • domain assumption Denotations of natural numbers are finitely supported sequences; the infinite sum in the iteration compiler is well-defined only under finite support.
    Stated in Section 4.2.1 as critical ('this summation is not well-defined without finite support'). It is essential for the compiler to be well-defined and for differentiability to be canonical.
  • standard math Context exchange (permuting variables in a context) is admissible in the typing and compiler.
    Invoked throughout Appendix B.8/B.10 via 'Because contexts permit exchange'; assumed without proof. Standard for linear type systems with context splitting.
  • domain assumption Linear type discipline forbidding contraction and weakening yields multilinear denotations.
    Section 3; the connection between linear programs and linear maps is taken from prior work [16,21], not re-derived in this paper.
  • standard math Barendregt convention: free and bound variable names are distinct.
    Used in Appendix proofs (B.8, B.10) to justify 'vacuous by Barendregt's convention'; a standard syntactic convention.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Compiling to recurrent neurons." pith.science (2026). https://pith.science/paper/EW2ZN6X5

@misc{pith2026251114953,
  author       = {Pith},
  title        = {Pith review of: Compiling to recurrent neurons},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EW2ZN6X5}},
  note         = {Machine review of arXiv:2511.14953}
}
abstract

Discrete structures are currently second-class in differentiable programming. Since functions over discrete structures lack overt derivatives, differentiable programs do not differentiate through them and limit where they can be used. For example, when programming a neural network, conditionals and iteration cannot be used everywhere; they can break the derivatives necessary for gradient-based learning to work. This limits the class of differentiable algorithms we can directly express, imposing restraints on how we build neural networks and differentiable programs more generally. However, these restraints are not fundamental. Recent work shows conditionals can be first-class, by compiling them into differentiable form as linear neurons. Similarly, this work shows iteration can be first-class -- by compiling to linear recurrent neurons. We present a minimal typed, higher-order and linear programming language with iteration called $\textsf{Cajal}\scriptstyle(\mathbb{\multimap}, \mathbb{2}, \mathbb{N})$. We prove its programs compile correctly to recurrent neurons, allowing discrete algorithms to be expressed in a differentiable form compatible with gradient-based learning. With our implementation, we conduct two experiments where we link these recurrent neurons against a neural network solving an iterative image transformation task. This determines part of its function prior to learning. As a result, the network learns faster and with greater data-efficiency relative to a neural network programmed without first-class iteration. A key lesson is that recurrent neurons enable a rich interplay between learning and the discrete structures of ordinary programming.

Figures

Figures reproduced from arXiv: 2511.14953 by the authors.

Figure 1
Figure 1. Iterative image transform Functions over discrete structures lack overt derivatives. Nev￾ertheless, they could be differentiated if compiled to differen￾tiable form, enabling discrete structure to appear anywhere in a differentiable program. But it is not yet clear how to build these compilers. For conditionals, recent work shows it is possible by compiling programs to linear neurons1 [20]. For iteration over natura… view at source ↗
Figure 2
Figure 2. Programming and compiling an iterative image transform [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. Linear recurrent neurons and their dynamics [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figures from the paper (22 more)
Figure 4
Figure 4. Figure 4: Programming with and without duplicating/discarding [PITH_FULL_IMAGE:figures/full_fig_p004_4.png]
Figure 5
Figure 5. Figure 5: Typing with and without duplicating/discarding [PITH_FULL_IMAGE:figures/full_fig_p005_5.png]
Figure 6
Figure 6. Figure 6: Correctly compiling to recurrent neurons [PITH_FULL_IMAGE:figures/full_fig_p005_6.png]
Figure 7
Figure 7. Figure 7: Syntax of Cajal(⊸, 2, N) 4.1.1 Syntax. Cajal(⊸, 2, N) is a minimal typed, higher-order and linear programming language [PITH_FULL_IMAGE:figures/full_fig_p006_7.png]
Figure 8
Figure 8. Figure 8: Evaluating Cajal(⊸, 2, N) programs Typing Δ ⊢ 𝑒 : 𝜏 ⇐⇒ program 𝑒 has type 𝜏 𝑥 :𝜏 ⊢ 𝑥 : 𝜏 ∅ ⊢ tt : 2 ∅ ⊢ ff : 2 ∅ ⊢ 0 : N Δ ⊢ 𝑒 : N Δ ⊢ succ(𝑒) : N Δ, 𝑥 :𝜏1 ⊢ 𝑒 : 𝜏2 Δ ⊢ 𝜆𝑥.𝑒 : 𝜏1 ⊸ 𝜏2 Δ1 ⊢ 𝑒1 : 𝜏1 ⊸ 𝜏2 Δ2 ⊢ 𝑒2 : 𝜏1 Δ1 ◦ Δ2 ⊢ 𝑒1𝑒2 : 𝜏2 Δ1 ⊢ 𝑒1 : 2 Δ2 ⊢ 𝑒2 : 𝜏 Δ2 ⊢ 𝑒3 : …
Figure 9
Figure 9. Figure 9: Typing Cajal(⊸, 2, N) programs 4.1.3 Typing. Cajal(⊸, 2, N) is linearly typed. The presence of context splitting in typing application, conditionals, and iteration ensures that the structural rule contraction is not permissible. This relation relates two contexts if th…
Figure 10
Figure 10. Figure 10: Logical Relation for Cajal(⊸, 2, N) At each type, the logical relation RE⟦𝜏⟧ returns a set of terminating Cajal(⊸, 2, N) expressions. It includes expressions which are not syntactically well-typed. For example, (if tt then tt else 0) ∈ RE⟦2⟧. We say these expression a…
Figure 11
Figure 11. Figure 11: Compiling Cajal(⊸, 2, N) types For natural numbers, the choice of vector space is more subtle. In [PITH_FULL_IMAGE:figures/full_fig_p009_11.png]
Figure 12
Figure 12. Figure 12: Compiling Cajal(⊸, 2, N) contexts 5By convention we denote elements of a compiled 1-tuple using 𝑥®, and elements of a compiled 𝑘-tuple as 𝜎® [PITH_FULL_IMAGE:figures/full_fig_p009_12.png]
Figure 13
Figure 13. Figure 13: Compiling Cajal(⊸, 2, N) programs Compiling variables is straight-forward. The variable rule maps to identity at each type. ⟦𝑥 :2 ⊢ 𝑥 : 2⟧ ↦→ (𝑥® ∈ R 2 ↦→ 𝑥®) Our specification in [PITH_FULL_IMAGE:figures/full_fig_p010_13.png]
Figure 14
Figure 14. Figure 14: Prototypical learning dynamics for Experiment 1 [PITH_FULL_IMAGE:figures/full_fig_p016_14.png]
Figure 15
Figure 15. Figure 15: Summary of dynamics across configurations for Experiment 1 [PITH_FULL_IMAGE:figures/full_fig_p017_15.png]
Figure 16
Figure 16. Figure 16: Summary of dynamics across configurations for Experiment 2 [PITH_FULL_IMAGE:figures/full_fig_p017_16.png]
Figure 17
Figure 17. Figure 17: Prototypical learning dynamics for Experiment 2 [PITH_FULL_IMAGE:figures/full_fig_p018_17.png]
Figure 18
Figure 18. Figure 18: XOR task C.1.1 Task. This experiment studies how neural networks learn a binary classification involving XOR logic, shown in [PITH_FULL_IMAGE:figures/full_fig_p039_18.png]
Figure 19
Figure 19. Figure 19: Summary of dynamics across configurations [PITH_FULL_IMAGE:figures/full_fig_p039_19.png]
Figure 20
Figure 20. Figure 20: EQ task C.2.1 Task. This experiment studies how neural networks learn a binary classification involving EQ logic, shown in [PITH_FULL_IMAGE:figures/full_fig_p040_20.png]
Figure 21
Figure 21. Figure 21: Summary of dynamics across configurations [PITH_FULL_IMAGE:figures/full_fig_p040_21.png]
Figure 22
Figure 22. Figure 22: AND task C.3.1 Task. This experiment studies how neural networks learn a binary classification involving AND logic, shown in [PITH_FULL_IMAGE:figures/full_fig_p041_22.png]
Figure 23
Figure 23. Figure 23: Summary of dynamics across configurations [PITH_FULL_IMAGE:figures/full_fig_p041_23.png]
Figure 24
Figure 24. Figure 24: OR Task C.4.1 Task. This experiment studies how neural networks learn a binary classification involving OR logic, shown in [PITH_FULL_IMAGE:figures/full_fig_p042_24.png]
Figure 25
Figure 25. Figure 25: Summary of dynamics across configurations [PITH_FULL_IMAGE:figures/full_fig_p042_25.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

26 extracted references · 1 linked inside Pith

  1. [20]

    Joey Velez-Ginorio, Nada Amin, Konrad Kording, and Steve Zdancewic. 2026. Compiling to linear neurons.Proceedings of the ACM on Programming Languages, POPL (2026)

    2026

  2. [5]

    Thomas Ehrhard. 2002. On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12, 5 (2002), 579–623

    2002

  3. [19]

    Benoît Valiron and Steve Zdancewic. 2014. Finite vector spaces as model of simply-typed lambda-calculi. InInternational Colloquium on Theoretical Aspects of Computing . Springer, 442–459

    2014

  4. [1]

    Martín Abadi and Gordon D Plotkin. 2019. A simple differentiable programming language. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–28

    2019

  5. [2]

    Panos J Antsaklis and Anthony N Michel. 2006. Linear systems. Springer

    2006

  6. [3]

    Matko Bosnjak, Tim Rocktaschel, Jason Naradowsky, and Sebastian Riedel. 2017. Programming with a differentiable forth interpreter. In International conference on machine learning . PMLR, 547–556

    2017

  7. [4]

    James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. 2018. JAX: composable transformations of Python+NumPy programs. http://github.com/jax-ml/jax

    2018

  8. [6]

    Conal Elliott. 2018. The simple essence of automatic differentiation.Proceedings of the ACM on Programming Languages 2, ICFP (2018), 1–29

    2018

Show all 26 references
  1. [7]

    Alexander L Gaunt, Marc Brockschmidt, Nate Kushman, and Daniel Tarlow. 2017. Differentiable programs with neural libraries. In International Conference on Machine Learning . PMLR, 1213–1222

    2017

  2. [8]

    Robert Harper. 2016. Practical foundations for programming languages . Cambridge University Press

    2016

  3. [9]

    Alain Hore and Djemel Ziou. 2010. Image quality metrics: PSNR vs. SSIM. In 2010 20th international conference on pattern recognition. IEEE, 2366–2369

    2010

  4. [10]

    Ozan Irsoy and Claire Cardie. 2014. Deep recursive neural networks for compositionality in language. Advances in neural information processing systems 27 (2014)

    2014

  5. [11]

    Diederik P Kingma. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014). Compiling to recurrent neurons 21

    2014 arXiv

  6. [12]

    Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A Eisenberg, and Andrew Fitzgibbon

  7. [13]

    Erwin Kreyszig. 1991. Introductory functional analysis with applications . John Wiley & Sons

    1991

  8. [14]

    Yann LeCun, Bernhard Boser, John Denker, Donnie Henderson, Richard Howard, Wayne Hubbard, and Lawrence Jackel

  9. [15]

    Ziyang Li, Jiani Huang, and Mayur Naik. 2023. Scallop: A language for neurosymbolic programming. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 1463–1487

    2023

  10. [16]

    Paul-André Mellies. 2009. Categorical semantics of linear logic. Panoramas et syntheses 27 (2009), 15–215

    2009

  11. [17]

    Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. 2019. Pytorch: An imperative style, high-performance deep learning library. Advances in neural information processing system...

    2019

  12. [18]

    Michael Spivak. 2018. Calculus on manifolds: a modern approach to classical theorems of advanced calculus . CRC press

    2018

  13. [21]

    David Walker. 2005. Substructural type systems. Advanced topics in types and programming languages (2005), 3–44

    2005

  14. [22]

    Glynn Winskel. 1993. The formal semantics of programming languages: an introduction . MIT press. 22 Joey Velez-Ginorio, Nada Amin, Konrad Paul Kording, and Steve Zdancewic A DEFINITIONS A.1 Context Splitting Δ = Δ1∪ Δ2 ∅ = dom(Δ1)∩ dom(Δ2) Δ = Δ1◦ Δ2 A.2 Length of a context le...

    1993

  15. [24]

    Model D is a neural network programmed using Cajal(⊸, 2, N), the AND structure is directly programmed using our compiler

    The input is two images𝑥1 and𝑥2: ⊲ If𝑥1 is even or𝑥2 is odd, return ✓ ⊲ Otherwise, return ✗ C.4.2 Models. Model D is a neural network programmed using Cajal(⊸, 2, N), the AND structure is directly programmed using our compiler. ⟦if𝑥 then(if𝑦 then tt else tt) else(if𝑦 then tt e...

    2000

  16. [25]

    Model D is a neural network programmed using Cajal(⊸, 2, N), the EQ structure is directly programmed using our compiler

    The input is two images𝑥1 and𝑥2: ⊲ If𝑥1 and𝑥2 are even, return ✓ ⊲ If𝑥1 and𝑥2 are odd, return ✓ ⊲ Otherwise, return ✗ C.2.2 Models. Model D is a neural network programmed using Cajal(⊸, 2, N), the EQ structure is directly programmed using our compiler. ⟦if𝑥 then(if𝑦 then tt el...

    2000

  17. [1989]

    Advances in neural information processing systems 2 (1989)

    Handwritten digit recognition with a back-propagation network. Advances in neural information processing systems 2 (1989)

    1989

  18. [2022]

    Proceedings of the ACM on Programming Languages 6, POPL (2022), 1–30

    Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation. Proceedings of the ACM on Programming Languages 6, POPL (2022), 1–30

    2022

Pith tools

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