Pith. sign in

REVIEW 3 major objections 5 minor 59 references

Neural Proof Nets

T0 review · 3 major / 5 minor · reviewed 2026-08-27 · deepseek-v4-flash

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

Pith's one-line read A Sinkhorn-based neural parser constructs proof nets that transcribe Dutch sentences into linear-logic proofs and lambda terms, with up to 70% term accuracy.

desk verdict A solid, well-engineered neuro-symbolic parser that turns raw Dutch text into linear logic proof nets via Sinkhorn-learned axiom links; the empirical claims hold up, but the modal proof-net correctness gap deserves explicit patching. read the letter →

arxiv 2009.12702 v1 pith:535WYHA7 submitted 2020-09-26 cs.CL cs.LGcs.LO

Konstantinos Kogkalidis , Michael Moortgat , Richard Moot This is my paper · ORCID
classification cs.CLcs.LGcs.LO
keywords linearlogicproofnetsSinkhornnetworkstype-logicalgrammarsupertagginglambdacalculusDutchparsingneuro-symbolic
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 claims that parsing a sentence can be carried out by constructing a proof net for its linear-logic types: a generative model first turns the words into a flat sequence of type symbols, and a Sinkhorn network then pairs matching atomic formulas into axiom links. Any structure that passes a standard traversal check is a formally valid proof, and its attached $\lambda$-term — the sentence's program for meaning composition — is obtained without further neural decoding. On a corpus of written Dutch, the full system recovers the correct typed, dependency-decorated $\lambda$-term for up to 67.6% of test sentences, and 69.6% when type labels are ignored. If this stands, it gives a fully differentiable, backtracking-free parser whose outputs are certified proofs rather than approximate trees.

What carries the argument

The central object is the proof net, a graph built from formula decomposition trees connected by axiom links pairing atoms of opposite polarity. The operative mechanism is the Sinkhorn operator, a differentiable iteration that drives a matrix toward a doubly-stochastic, near-binary permutation matrix. The paper uses this operator to predict how negative and positive occurrences of each atomic type should be aligned, then applies a correctness traversal that checks connectedness and acyclicity, certifying the result as a proof net.

What would settle it

Construct a case where a proof structure passes the traversal check but does not correspond to a valid derivation in the modal system — for example, a dependency modality that would require different polarity information than the flat symbol stream encodes. If such a case exists, the validation step would accept structures that are not genuine proofs.

Watch

Extended reading notes

Core claim

The central claim is that proof search in the implication-only fragment of intuitionistic linear logic can be reduced to two learned steps: decoding a proof frame (the formula decomposition tree written as a symbol sequence) and finding a permutation of atomic occurrences of each type that respects the logic's invariants. The permutation is learned as a soft doubly-stochastic matrix produced by iterated row/column normalization, then discretized and checked by the traversal algorithm for proof nets. Accepted structures map to $\beta$-normal $\eta$-long $\lambda$-terms through the isomorphism between linear proofs and linear programs. The authors report up to 69.6% untyped term accuracy at beam width 7, and 85.4% when the gold proof frame is supplied, indicating that the remaining errors are dominated by type decoding rather than by link prediction.

Load-bearing premise

The load-bearing premise is that the proof-net correctness test, which is sound and complete for the implication-only logic, remains valid for the richer modal type system used in the corpus; the paper offers no proof or citation for this extension.

Editorial extensions

If this is right

  • Proof search in this fragment of linear logic becomes an alignment problem, so any model that can score pairs of atomic occurrences can be trained end-to-end to produce certified derivations.
  • Because each $\lambda$-term is read from a certified proof net rather than decoded symbol-by-symbol, every validated output is a type-safe program skeleton in $\beta$-normal $\eta$-long form.
  • Beam search combined with logical filtering lets the system discard high-scoring but invalid parses, making the validity check a hard constraint.
  • The gap between frame correctness (70.2%) and typed term accuracy (67.6%), and the jump to 85.4% with gold frames, indicates that improving the generative supertagger would directly improve end-to-end accuracy.

Reading between the lines

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

  • A natural extension is to test the same permutation-learning setup on richer fragments of linear logic, such as those with multiplicative connectives, where the flat symbol encoding would need additional structure.
  • The bipartite matching view suggests that replacing dot-product attention with a more constrained optimal-transport plan could improve link accuracy, though the paper does not investigate this.
  • Even a partially correct derivation might carry usable meaning information; a task-based evaluation, such as using derived terms for natural-language inference, could reveal practical signal beyond exact-match accuracy.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Request a human review

A listed scientist reviews the paper for a fee and the review publishes here regardless of verdict. See the reviewers or get listed.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper introduces 'Neural Proof Nets', an end-to-end differentiable parser that (i) supertags Dutch sentences into flattened proof frames over the dependency-decorated type system ILL⊸,3,2 using a sequence-to-sequence decoder, and (ii) predicts axiom-link permutations with a Sinkhorn layer over contextualized atom representations. The resulting proof structures are checked with Lamarche's traversal and converted to linear λ-terms. On the Æthel dataset, with beam search and grammar-based filtering, the model reaches about 70% typed term accuracy and about 85.4% term accuracy when ground-truth frames are supplied, compared with an Alpino baseline of 45.7% untyped term accuracy. The authors argue that the generated λ-terms are not themselves the product of neural decoding but a corollary of the isomorphism between ILL⊸ proofs and linear λ-calculus programs.

Significance. If the formal claims hold, this is a valuable neuro-symbolic parsing result: it is among the first neural systems to produce formally certified proof nets and λ-terms for a type-logical grammar, and the Sinkhorn formulation of axiom linking is clean, batch-efficient, and well matched to the combinatorial structure of proof search. The paper's strengths include held-out exact-match evaluation on Æthel, a disclosed filtering rule, an oracle-type experiment isolating supertagging as the bottleneck, and released code. The main scientific risk is that the formal certificate is stated for ILL⊸ while the experimental target is ILL⊸,3,2; this gap must be resolved before the stronger 'proofs and terms of the linear λ-calculus' claim is accepted.

major comments (3)
  1. [§2.2, §4.2] The paper validates decoded structures with Lamarche's essential-net criterion, but the object language of the experiments is ILL⊸,3,2, whose unary modalities 3d and 2m are flattened into the proof-frame symbol stream (Figure 3 caption; Section 3.1). The manuscript does not state whether modal markers are erased before the Lamarche traversal or retained as first-class graph nodes, and it provides no soundness or completeness argument, nor a citation, for applying the ILL⊸ correctness criterion to this modal extension. Because the abstract and Section 5 claim that the outputs are proofs and linear λ-terms, this gap is load-bearing; the authors should either prove or cite the appropriate correctness criterion for ILL⊸,3,2, or explicitly restrict the formal claim to the plain ILL⊸ skeleton and describe the dependency-decorated output as a separate projection.
  2. [§3.2, Sinkhorn equations] The displayed Sinkhorn definition is not self-consistent as written. The operator Tr is called row normalization, but the displayed formula subtracts the log of a sum over the row index r for a fixed column j, using max(X_{r,:}) inside the sum; this is neither a standard row nor a standard column softmax, and the alternating composition Tr(Tr(·)^T) therefore does not have the stated effect. Additionally, Sinkhorn0(X)=X is not in log space while the recursion applies log-space normalizations, so the domain of the iterates and the role of the final exponential are ambiguous. Since the Sinkhorn layer is the core permutation mechanism, the authors should correct the indices and state the log-domain convention precisely so that the algorithm is reproducible from the equations alone.
  3. [§4.3, Table 1] The headline accuracy figures are point estimates from a single training run: no seed variation, error bars, or significance tests are reported, and model selection is performed on the validation set using the same metrics. Given that the differences between beam sizes 3 and 7 are only a few tenths of a point, the central empirical claim would be substantially strengthened by reporting variance over at least a few seeds or by explicitly stating that the results are single-run.
minor comments (5)
  1. [§4.3] Please clarify in the text that 'first valid beam' means the highest-scoring beam that passes the logical filters, not an oracle selection with access to the correct label; the current phrasing could be misread as selecting a beam by its correctness.
  2. [Table 1] Please report, for each beam size, the proportion of test samples for which no beam satisfies the logical filters, since those samples are automatically counted as failures and the proportion affects how the filtering rule interacts with the reported accuracies.
  3. [§A.2] The paper states that Sinkhorn iterations are set to 5 during training but does not state the number of iterations used at inference; please specify this in the experimental setup.
  4. [§3.1, Table 2] The exact symbol vocabulary V is not defined explicitly: the decoder vocabulary size is reported as 58, but the text only says V is the union of atomic types and dependency-decorated modal markings; please list or precisely characterize the 58 symbols.
  5. [§4.1] The validation metric 'linking accuracy under the assumption of an error-free decoding' is mentioned but not reported; either report it or state explicitly that it is used only for model selection.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the architecture is trained and evaluated on held-out data, and the claimed λ-term extraction is a deterministic corollary of proof-net validation rather than a fitted output.

full rationale

The paper's central claims are empirical accuracy numbers on a held-out test set of the Æthel dataset, with the model trained on separate training and validation splits. The Sinkhorn layer is trained against gold permutation matrices, but test-time metrics such as frame correctness, untyped term accuracy, and typed term accuracy measure generalization to unseen sentences; no fitted parameter is renamed as a prediction. The self-citations to Kogkalidis et al. (2019, 2020) supply the generative supertagging paradigm and the dataset/extraction procedure, but these function as empirical resources and baselines, not as load-bearing mathematical assumptions that force the reported results. The proof-net correctness check and λ-term extraction cite external work (Lamarche 2008; de Groote and Retoré 1996), and the statement that generated λ-terms are a corollary of the ILL⊸/linear-λ isomorphism relies on the standard Curry-Howard correspondence, not on the model's own fitted values. A formal caveat is present but not circular: the paper does not explicitly prove that Lamarche's essential-net criterion for ILL⊸ is sound and complete for the modal system ILL⊸,3,2, since dependency-decorated modal markings are flattened into the proof-frame symbol stream; this is a verification gap, not a reduction of the derivation to its inputs. Overall, the derivation chain is self-contained with respect to the empirical evaluation, and no circular step was identified.

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

The central claim is an empirical ML result, so the main free parameters are the trained network weights and selected hyperparameters, all fitted to the Æthel training set rather than derived. The formal background (Sinkhorn theorem, Curry-Howard, proof-net correctness) is standard and cited. The least justified input is the extension of ILL⊸ proof-net validation to the modal types 3 and 2, which the paper assumes without proof. No new physical or theoretical entities are postulated.

free parameters (7)
  • Learned network parameters (BERTje, decoder, bi-modal encoder, projections) = trained on 55,683 Æthel training samples
    All reported accuracy depends on these fitted weights; this is supervised learning rather than a parameter-free derivation.
  • Sinkhorn iterations = 5
    Set during training; fewer iterations hurt convergence and more risk vanishing gradients (Appendix A.2).
  • Label smoothing = 0.1
    Optimization hyperparameter selected on validation data (Appendix A.2).
  • Warmup epochs = 5
    Learning-rate warmup in the Vaswani schedule, selected on validation (Appendix A.2).
  • BERT learning-rate scale = 0.1
    Scales the learning rate for BERT parameters relative to the decoder; chosen by grid search (Appendix A.2).
  • Proof frame length filter = frames up to 100 primitive symbols
    Only samples with proof frames under 100 symbols are kept, about 97% of the dataset; this bounds the reported accuracy (Section 4.1, A.3).
  • Beam size = 1, 2, 3, 5, 7
    Accuracy is reported for different beam widths using the first logically valid beam (Section 4.2).
assumptions (5)
  • standard math Sinkhorn's theorem: iterative row and column normalization of a positive square matrix converges to a doubly-stochastic matrix.
    Underlies the continuous relaxation of permutation matrices in Section 3.2.
  • standard math Curry-Howard isomorphism for intuitionistic linear logic: proofs correspond to linear lambda terms.
    Used to extract lambda terms from proof nets in Sections 2.1 and 4.2; cited background.
  • standard math Proof-net correctness criteria (Danos-Regnier, Lamarche) are sound and complete for multiplicative intuitionistic linear logic proof nets, and validation is linear-time.
    The filtering step in Section 4.2 relies on Lamarche's traversal to accept or reject decoded proof structures.
  • domain assumption Æthel's automatically extracted derivations, with manual correction, are an accurate ground truth for Dutch type-logical grammar.
    Training and test targets come from this dataset; systematic extraction errors would be inherited by the reported accuracies.
  • ad hoc to paper The modal type system ILL⊸,3,2 can be faithfully represented and validated by ILL⊸ proof nets, with unary modalities flattened into the symbol stream.
    No formal proof or citation is given for this extension; Figure 3 shows modal markings in place of implication arrows, and validation uses Lamarche's ILL⊸ traversal.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Neural Proof Nets." pith.science (2026). https://pith.science/paper/535WYHA7

@misc{pith2026200912702,
  author       = {Pith},
  title        = {Pith review of: Neural Proof Nets},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/535WYHA7}},
  note         = {Machine review of arXiv:2009.12702}
}
read the original abstract

Linear logic and the linear {\lambda}-calculus have a long standing tradition in the study of natural language form and meaning. Among the proof calculi of linear logic, proof nets are of particular interest, offering an attractive geometric representation of derivations that is unburdened by the bureaucratic complications of conventional prooftheoretic formats. Building on recent advances in set-theoretic learning, we propose a neural variant of proof nets based on Sinkhorn networks, which allows us to translate parsing as the problem of extracting syntactic primitives and permuting them into alignment. Our methodology induces a batch-efficient, end-to-end differentiable architecture that actualizes a formally grounded yet highly efficient neuro-symbolic parser. We test our approach on {\AE}Thel, a dataset of type-logical derivations for written Dutch, where it manages to correctly transcribe raw text sentences into proofs and terms of the linear {\lambda}-calculus with an accuracy of as high as 70%.

Figures

Figures reproduced from arXiv: 2009.12702 by the authors.

Figure 1
Figure 1. Example derivation and Curry-Howard λ-term for the phrase De strategie die ze volgen is eeuwenoud (“The strategy that they follow is ancient”) from Æthel sample dpc-ind-001645-nl-sen.p.12.s.1_1, showcasing how hypothetical reasoning enables the derivation of an object-relative clause (note how the instanti￾ation of variable x of type PRON followed by its subsequent abstraction creates an argument for the higher-orde… view at source ↗
Figure 4
Figure 4. Shallow graph for the term of Figure [PITH_FULL_IMAGE:figures/full_fig_p003_4.png] view at source ↗
Figure 2
Figure 2. Links for linear logic proof nets. Left/right: positive/negative implication. Center: axiom link. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figures from the paper (4 more)
Figure 3
Figure 3. Figure 3: Proof net corresponding to the natural deduction derivation of Figure [PITH_FULL_IMAGE:figures/full_fig_p004_3.png]
Figure 5
Figure 5. Figure 5: An alternative view of the axiom links of Figure [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: Schematic diagram of the full network architecture. The supertagger (orange, left) iteratively generates [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: log2-transformed cumulative distributions of symbol and word lengths, counts of atomic formulas, ma￾trices and matrix sizes from the portion of the dataset trained on [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

59 extracted references · 46 canonical work pages

  1. [1]

    URL: " 'urlintro :=

    ENTRY address author booktitle chapter edition editor howpublished institution journal key month note number organization pages publisher school series title type volume year eprint doi pubmed url lastchecked label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block STRINGS urlintro eprinturl eprintpr...

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  3. [3]

    Lasha Abzianidze. 2016. https://doi.org/10.18653/v1/S16-2007 Natural solution to F ra C a S entailment problems . In Proceedings of the Fifth Joint Conference on Lexical and Computational Semantics, pages 64--74, Berlin, Germany. Association for Computational Linguistics

    work page doi:10.18653/v1/s16-2007 2016

  4. [4]

    Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E Hinton. 2016. Layer normalization. arXiv preprint arXiv:1607.06450v1

    work page Pith review arXiv 2016

  5. [5]

    Srinivas Bangalore and Aravind K Joshi. 1999. Supertagging: An approach to almost parsing. Computational linguistics, 25(2):237--265

    work page 1999

  6. [6]

    Aditya Bhargava and Gerald Penn. 2020. https://www.aclweb.org/anthology/2020.repl4nlp-1.23 Supertagging with CCG primitives . In Proceedings of the 5th Workshop on Representation Learning for NLP, pages 194--204, Online. Association for Computational Linguistics

    work page 2020

  7. [7]

    Gosse Bouma and Gertjan van Noord. 2017. https://www.aclweb.org/anthology/W17-0403 Increasing return on annotation investment: The automatic construction of a U niversal D ependency treebank for D utch . In Proceedings of the N o D a L i D a 2017 Workshop on Universal Dependencies ( UDW 2017) , pages 19--26, Gothenburg, Sweden. Association for Computation...

    work page 2017

  8. [8]

    Gosse Bouma, Gertjan van Noord, and Robert Malouf. 2001. Alpino: Wide-coverage computational analysis of dutch. In Computational linguistics in the Netherlands 2000, pages 45--59. Brill Rodopi

    work page 2001

Show all 59 references
  1. [9]

    Nicolaas Govert de Bruijn. 1979. Wiskundigen, let op uw N ederlands. Euclides, 55(juni/juli):429--435

    1979

  2. [10]

    Jan Buys and Phil Blunsom. 2017. Robust incremental neural semantic graph parsing. In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 1215--1226

    2017

  3. [11]

    Wanxiang Che, Yijia Liu, Yuxuan Wang, Bo Zheng, and Ting Liu. 2018. https://doi.org/10.18653/v1/K18-2005 Towards better UD parsing: Deep contextualized word embeddings, ensemble, and treebank concatenation . In Proceedings of the C o NLL 2018 Shared Task: Multilingual Parsing ...

    2018 doi

  4. [12]

    Jianpeng Cheng, Siva Reddy, Vijay Saraswat, and Mirella Lapata. 2019. Learning an executable neural semantic parser. Computational Linguistics, 45(1):59--94

    2019

  5. [13]

    Vincent Danos and Laurent Regnier. 1989. The structure of multiplicatives. Archive for Mathematical Logic, 28:181--203

    1989

  6. [14]

    Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2019. Bert: Pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human...

    2019

  7. [15]

    Li Dong and Mirella Lapata. 2016. Language to logical form with neural attention. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 33--43

    2016

  8. [16]

    Jean-Yves Girard. 1987. Linear logic. Theoretical computer science, 50(1):1--101

    1987

  9. [17]

    Jean-Yves Girard, Yves Lafont, and P. Taylor. 1988. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press

    1988

  10. [18]

    Philippe de Groote. 2001. Towards abstract categorial grammars. In Proceedings of the 39th Annual Meeting of the Association for Computational Linguistics, pages 252--259

    2001

  11. [19]

    Philippe de Groote and Christian Retor \'e . 1996. https://hal.archives-ouvertes.fr/hal-00823554 On the semantic readings of proof-nets . In Proceedings Formal grammar , pages 57--70, Prague, Czech Republic. FoLLI

    1996

  12. [20]

    Aditya Grover, Eric Wang, Aaron Zweig, and Stefano Ermon. 2019. https://openreview.net/forum?id=H1eSS3CcKX Stochastic optimization of sorting networks via continuous relaxations . In International Conference on Learning Representations

    2019

  13. [21]

    Stefano Guerrini. 1999. Correctness of multiplicative proof nets is linear. In Fourteenth Annual IEEE Symposium on Logic in Computer Science , pages 454--263. IEEE Computer Science Society

    1999

  14. [22]

    Dan Hendrycks and Kevin Gimpel. 2016. Bridging nonlinearities and stochastic regularizers with gaussian error linear units

    2016

  15. [23]

    Tao Ji, Yuanbin Wu, and Man Lan. 2019. Graph-based dependency parsing with graph neural networks. In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics, pages 2475--2485

    2019

  16. [24]

    Kanovich

    Max I. Kanovich. 1994. The complexity of horn fragments of linear logic. Annals of Pure and Applied Logic, 69(2-3):195--241

    1994

  17. [25]

    Konstantinos Kogkalidis, Michael Moortgat, and Tejaswini Deoskar. 2019. Constructive type-logical supertagging with self-attention networks. In Proceedings of the 4th Workshop on Representation Learning for NLP (RepL4NLP-2019), pages 113--123

    2019

  18. [26]

    Konstantinos Kogkalidis, Michael Moortgat, and Richard Moot. 2020. https://www.aclweb.org/anthology/2020.lrec-1.647 Æthel: Automatically extracted typelogical derivations for dutch . In Proceedings of The 12th Language Resources and Evaluation Conference, pages 5259--5268, Mar...

    2020

  19. [27]

    Ysuke Kubota and Robert Levine. 2020. Type-Logical Syntax. MIT Press

    2020

  20. [28]

    Fran c ois Lamarche. 2008. https://hal.inria.fr/inria-00347336/file/prfnet1.pdf Proof nets for intuitionistic linear logic: Essential nets . Research report, INRIA Nancy

    2008

  21. [29]

    Joachim Lambek. 1958. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154--170

    1958

  22. [30]

    Zuchao Li, Jiaxun Cai, Shexia He, and Hai Zhao. 2018. Seq2seq dependency parsing. In Proceedings of the 27th International Conference on Computational Linguistics, pages 3203--3214

    2018

  23. [31]

    Patrick Lincoln. 1995. Deciding provability of linear logic formulas. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, pages 109--122. Cambridge University Press

    1995

  24. [32]

    Jiangming Liu, Shay B Cohen, and Mirella Lapata. 2018. Discourse representation structure parsing. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 429--439

    2018

  25. [33]

    Ilya Loshchilov and Frank Hutter. 2018. Fixing weight decay regularization in adam

    2018

  26. [34]

    Gonzalo Mena, David Belanger, Scott Linderman, and Jasper Snoek. 2018. https://openreview.net/forum?id=Byt3oJ-0W Learning latent permutations with G umbel- S inkhorn networks . In International Conference on Learning Representations

    2018

  27. [35]

    Michael Moortgat. 1996. Multimodal linguistic inference. Journal of Logic, Language and Information, 5(3/4):349--385

    1996

  28. [36]

    Glyn Morrill. 2014. A categorial type logic. In Categories and Types in Logic, Language, and Physics - Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, volume 8222 of Lecture Notes in Computer Science, pages 331--352. Springer

    2014

  29. [37]

    Rafael M \"u ller, Simon Kornblith, and Geoffrey E Hinton. 2019. When does label smoothing help? In Advances in Neural Information Processing Systems, pages 4696--4705

    2019

  30. [38]

    Murawski and C.-H

    Andrzej S. Murawski and C.-H. Luke Ong. 2000. Dominator trees and fast verification of proof nets. In Logic in Computer Science, pages 181--191

    2000

  31. [39]

    Reinhard Muskens. 2001. Lambda grammars and the syntax-semantics interface. In Proceedings of the 13th Amsterdam Colloquium, pages 150--155

    2001

  32. [40]

    Reinhard Muskens and Mehrnoosh Sadrzadeh. 2018. Static and dynamic vector semantics for lambda calculus models of natural language. Journal of Language Modelling, 6(2):319--351

    2018

  33. [41]

    Gertjan van Noord, Gosse Bouma, Frank van Eynde, Daniel de Kok, Jelmer van der Linde, Ineke Schuurman, Erik Tjong Kim Sang, and Vincent Vandeghinste. 2013. Large scale syntactic annotation of written dutch: Lassy. In Essential speech and language technology for Dutch, pages 14...

    2013

  34. [42]

    Ofir Press and Lior Wolf. 2017. Using the output embedding to improve language models. In Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 2, Short Papers, pages 157--163

    2017

  35. [43]

    Dirk Roorda. 1991. Resource Logics: Proof-theoretical Investigations. Ph.D. thesis, Universiteit van Amsterdam

    1991

  36. [44]

    Richard Sinkhorn. 1964. A relationship between arbitrary positive matrices and doubly stochastic matrices. The annals of mathematical statistics, 35(2):876--879

    1964

  37. [45]

    Morten Heine S rensen and Pawel Urzyczyn. 2006. Lectures on the Curry-Howard isomorphism. Elsevier

    2006

  38. [46]

    Kyle Swanson, Lili Yu, and Tao Lei. 2020. Rationalizing text matching: Learning sparse alignments via optimal transport. arXiv preprint arXiv:2005.13111

    2020 arXiv

  39. [47]

    Yi Tay, Dara Bahri, Liu Yang, Donald Metzler, and Da-Cheng Juan. 2020. Sparse sinkhorn attention. arXiv preprint arXiv:2002.11296v1

    2020 arXiv

  40. [48]

    Anne Sjerp Troelstra and Helmut Schwichtenberg. 2000. Basic Proof Theory, 2 edition, volume 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press

    2000

  41. [49]

    Ashish Vaswani, Yonatan Bisk, Kenji Sagae, and Ryan Musa. 2016. Supertagging with lstms. In Proceedings of the 2016 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pages 232--237

    2016

  42. [50]

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, ukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In Advances in neural information processing systems, pages 5998--6008

    2017

  43. [51]

    Wietse de Vries, Andreas van Cranenburgh, Arianna Bisazza, Tommaso Caselli, Gertjan van Noord, and Malvina Nissim. 2019. BERT je: A D utch BERT model. arXiv preprint arXiv:1912.09582v1

    2019 arXiv

  44. [52]

    Philip Wadler. 1993. A taste of linear logic. In International Symposium on Mathematical Foundations of Computer Science, pages 185--210. Springer

    1993

  45. [53]

    Benyou Wang, Donghao Zhao, Christina Lioma, Qiuchi Li, Peng Zhang, and Jakob Grue Simonsen. 2020. https://openreview.net/forum?id=Hke-WTVtwr Encoding word order in complex embeddings . In International Conference on Learning Representations

    2020

  46. [54]

    Sam Wiseman and Alexander M Rush. 2016. Sequence-to-sequence learning as beam-search optimization. In Proceedings of the 2016 Conference on Empirical Methods in Natural Language Processing, pages 1296--1306

    2016

  47. [55]

    Chunyang Xiao, Marc Dymetman, and Claire Gardent. 2016. Sequence-based structured prediction for semantic parsing. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 1341--1350

    2016

  48. [56]

    Wenduan Xu, Michael Auli, and Stephen Clark. 2015. Ccg supertagging with a recurrent neural network. In Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing (Volume 2: ...

    2015

  49. [57]

    Luke S Zettlemoyer and Michael Collins. 2012. Learning to map sentences to logical form: Structured classification with probabilistic categorial grammars. arXiv preprint arXiv:1207.1420v1

    2012 arXiv

  50. [58]

    Sheng Zhang, Xutai Ma, Kevin Duh, and Benjamin Van Durme. 2019. https://doi.org/10.18653/v1/P19-1009 AMR parsing as sequence-to-graph transduction . In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics, pages 80--94, Florence, Italy. Assoc...

    2019 doi

  51. [59]

    Xingxing Zhang, Jianpeng Cheng, and Mirella Lapata. 2017. Dependency parsing as head selection. In Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 1, Long Papers, pages 665--676

    2017

Pith tools

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