Pith. sign in

REVIEW 4 major objections 5 minor 52 references

Grounded Language Design for Lightweight Diagramming for Formal Methods

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

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

Pith's one-line read This paper proposes a small diagramming language, Cope and Drag (CnD), that refines model finders' default node-edge output with a few hard constraints, and shows in user studies that the resulting diagrams help people reason about…

desk verdict A genuinely useful DSL for Forge/Alloy diagramming with solid but narrow comprehension evidence; the 'lightweight to author' claim is so far unmeasured. read the letter →

arxiv 2412.03310 v1 pith:2N2KZN4V submitted 2024-12-04 cs.CL cs.PL

Siddhartha Prasad , Ben Greenman , Tim Nelson , Shriram Krishnamurthi This is my paper · ORCID
classification cs.CLcs.PL
keywords lightweightformalmethodsdiagramminglanguageAlloymodelfindingvisualizationdomain-specificcognitivescienceofdiagramsbadinstances
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

Model-finding tools like Alloy present their instances as generic node-edge graphs that grow confusing as specifications grow, while hand-written custom visualizations demand JavaScript expertise and can silently hide the very errors a user is hunting for. This paper argues that the right fix is a small language dedicated to lightweight diagramming, and presents Cope and Drag (CnD), whose primitives capture relative positioning, grouping, and pictorial styling. The design is grounded top-down in Gestalt and pre-attentive processing principles and bottom-up in an analysis of 58 student projects that shows what domain experts actually draw. In user studies, participants answered instance-understanding questions more accurately with CnD diagrams than with Alloy's default visualizer (62.75% vs 48.04%), and they were significantly better at noticing and explaining bad instances (71.43% vs 43.24%). If the results hold, model finding stays lightweight because users get meaningful diagrams without leaving the declarative spirit.

What carries the argument

The load-bearing mechanism is a deliberately small grammar of diagramming operations—relative positioning (orientation and cyclic constraints), grouping, and styling directives—each traceable to a named perceptual or diagramming principle such as Gestalt proximity, pre-attentive processing, or cognitive load, and each confirmed by the corpus of student visualizations. CnD applies these as hard constraints on top of the default node-edge graph; the Cassowary linear constraint solver checks satisfiability and WebCola lays out the result, so when constraints conflict the tool reports an error instead of drawing something wrong.

What would settle it

A concrete test: take a fresh corpus of custom visualizations from a different institution or from practitioners and express each one in CnD; if a substantial share needs a layout operation outside orientation, cyclic, grouping, and styling, the claimed niche is not general.

Watch

Extended reading notes

Core claim

The central claim is that diagramming for formal methods can be expressed as a small set of orthogonal, declarative primitives applied as hard constraints on top of a default visualizer's output, and that this is enough to produce diagrams that are both easier to reason with and safer for bad instances than either generic defaults or full custom code. CnD's primitives are cyclic constraints (arrange atoms along a circle), orientation constraints (place atoms above, below, left, or right of each other), grouping constraints (enclose related atoms in boxes and collapse edges), and directives for icons, colors, attributes, projection, and hiding disconnected nodes. Constraints are hard: inconsistent or unsatisfiable layouts produce an error message rather than a misleading diagram. The evaluation supports the claim with two significant results: CnD improved instance-understanding accuracy and improved identification and explanation of bad instances relative to the Alloy Default Visualizer.

Load-bearing premise

The design assumes that the diagramming needs of lightweight formal methods are well represented by 58 student projects from one course, so the primitives distilled from that corpus are sufficient for other domains and users.

Editorial extensions

If this is right

  • Users of Alloy-like tools can produce domain-meaningful diagrams from a few declarative rules, with no JavaScript or drawing-library expertise, so the incremental 'pay-as-you-go' character of lightweight formal methods is preserved.
  • Bad instances are handled safely: a constraint violation yields an explicit error message, and when a diagram is produced it does not hide the offending structure the way an expert-authored custom visualization can.
  • Because the empty CnD program reproduces the default visualizer exactly, users can refine diagrams one rule at a time and toggle rules on and off while exploring.
  • The same diagramming primitives can be carried to other formal-methods settings that show instances or counterexample traces, such as model checkers and proof assistants.
  • CnD occupies a new niche between generic visualizers and full drawing systems: it has the low floor of a default view and a moderate ceiling, avoiding both confusing defaults and brittle custom code.

Reading between the lines

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

  • The paper leaves implicit that CnD's error messages could double as spec-debugging hints: when an instance violates a layout constraint, the offending field and direction identify the structure the spec failed to constrain, and that could be tested as a teaching aid.
  • A testable extension would check whether pictorial directives help most for novices or for non-native speakers, since the icon study's accuracy gain (86.67% vs 73.33%) did not reach significance with a sample of 30.
  • One could try to infer CnD primitives automatically from existing custom visualization code, treating the student corpus as a training set; the paper explicitly doubts LLM-based generation, but example-based inference from diagrams is a different, untested route.
  • Applied to other model finders, a natural experiment would be to re-run the same task designs with ProB or Lean visualizations to see whether orientation, cyclic, grouping, and styling remain sufficient outside Alloy's relational idiom.
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 proposes Cope and Drag (CnD), a small DSL for custom diagramming of model-finder instances, layered on top of Alloy/Forge default visualizers. The design is grounded in cognitive-science principles and a corpus of 58 student projects; its primitives are cyclic/orientation constraints, grouping, and directives. The evaluation has two parts: author-authored CnD programs for external Alloy models, and three user studies comparing CnD diagrams against default visualizations on instance understanding, icon use, and bad-instance detection. The studies report significant advantages in comprehension (62.75% vs. 48.04%, p<0.05, d=0.26) and bad-instance detection (71.43% vs. 43.24%, p=0.03), but they do not test whether the target users can author CnD programs.

Significance. If the effectiveness results hold, CnD is a useful contribution to lightweight formal methods: it offers an incremental, declarative middle ground between generic graphs and D3-like programming, with hard-constraint failure instead of silent misrendering. Strengths include the bottom-up grounding in an external corpus, the use of test-set examples from the Alloy Models repository, the availability of interactive supplements and study instruments, and the fact that the effectiveness studies use scenarios not in the training corpus. The central risk is that the 'lightweight' authoring claim is unsupported by the evaluation: all user studies measure reading of author-authored diagrams, not writing or editing CnD programs.

major comments (4)
  1. [§5.2 vs. §3.3] The paper's central 'lightweight' claim is not tested. All three studies in §5.2 ask participants to read diagrams that the authors produced; none asks participants to write or edit a CnD program. The evidence for authoring ease in §3.3 is limited to the small grammar and the authors' own examples (§5.1). The quotes in §2.4 document D3's difficulty, but there is no control condition showing that CnD is easier. Because the title and abstract make 'lightweight' a core contribution, the report should be conditional on either adding an authoring study (e.g., comparing time and success for adding a constraint to a default visualization vs. the analogous D3/Sterling task) or reframing the claims as being about reading rather than writing diagrams.
  2. [§7] The claim in §7 that 'CnD diagrams are always at least as informative as Alloy Default Visualizer diagrams, and never less so' is contradicted by §3.2, where unsatisfiable constraints cause CnD to produce no diagram, and by Fig. 8, where the CnD response to a bad instance is an error rather than a diagram. An explicit error may be diagnostically better, but it is not the same as showing the instance. Also, §7 says CnD constraints 'cannot add new information not reflected in the Alloy Default Visualizer diagram,' while the footnote to that sentence says pictorial directives can communicate new information; these statements should be reconciled.
  3. [§5.2.1, Table 1] Table 1 shows large variation across the three scenarios: the pooled significance (62.75% vs. 48.04%, Z=2.30, p<0.05) appears to be driven mainly by the subway scenario (31% vs. 56%), while cards shows 28% vs. 36% and fruit 69% vs. 74%. Because each scenario tests a different primitive, the paper should report per-scenario inference or justify pooling with a pre-specified analysis, and should include exact p-values and confidence intervals. Without this, it is hard to tell which primitive is responsible for the reported effect.
  4. [§5.2.3] The bad-instance study uses only two familiar domains and the main comparison excludes participants who responded 'uncertain'; the paper should report the number of judgements excluded in each condition and discuss whether excluding uncertainty could bias the significant result toward the condition with fewer uncertain responses. This is particularly relevant because the paper itself notes that uncertainty may be a reasonable response rather than a wrong answer.
minor comments (5)
  1. [§2.1.1] There is a duplicated phrase: 'the brain often automatically processes demonstrates that the brain often automatically processes text'; this should be corrected.
  2. [§5.2.1] The paper uses 'Alloy Default Visualizer' as a blanket term for both Alloy Visualizer and Sterling, but in the study description it switches to 'Sterling' (e.g., 'than those shown Sterling visualizations'); define the terminology once at the start of the evaluation and use it consistently.
  3. [§5.2.1] The statistical reporting for the main comprehension result gives only 'Z=2.30, p<0.05'; report the test name and a precise p-value or confidence interval.
  4. [§6] The abstract says the paper 'compare[s] this against many other drawing languages and tools to show that this work defines a new niche,' but §6 is a qualitative comparison with no task-based benchmark; 'show' is stronger than the evidence supports.
  5. [§2.2] The bottom-up corpus comes from 58 projects in one course at one institution; a sentence in the limitations section acknowledging the representativeness risk would be useful for readers who want to transfer the primitives to other domains.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the design is grounded in external literature and a student-project corpus, and the effectiveness studies use new scenarios rather than the training set.

full rationale

The central derivation chain is grounded in external artifacts rather than in the paper's own conclusion. Section 2.1 takes diagramming operations from cognitive-science and visualization literature (e.g., Gestalt principles, Ma'ayan et al.'s tool requirements); Section 2.2 adds a corpus of 58 student projects from the Forge course; Section 2.3 aligns these into the CnD primitives. The key effectiveness claims in Section 5.2 are evaluated with new scenarios (cards, subway, fruit, tic-tac-toe, face) not drawn from that corpus, with random assignment against the Alloy Default Visualizer baseline and statistical tests; no parameter is fitted to those outcomes and then renamed as a prediction. Section 5.1 explicitly separates the 'training set' examples from a 'test set' drawn from the public Alloy Models repository, and the bad-instance studies in Section 5.2.3 use universally familiar scenarios rather than the training corpus. The paper's self-citations ([10], [30]) supply the student-project dataset and prior observations about custom-visualization failure modes; these are external empirical artifacts, not a uniqueness theorem or an ansatz citation, so they do not make the effectiveness result circular. The 'lightweight authoring' promise (Sections 2.4, 3.3) is indeed not directly evaluated by the comprehension studies, and the threats-to-validity section acknowledges that participants were not formal-methods experts; but that is an evidence gap, not a circular derivation. No equation, fitted parameter, or definition in the paper reduces the claimed result to its own inputs.

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

The paper introduces a programming language and its primitives, not a new physical or formal entity, so no invented entities apply. No numerical free parameters are fitted; the design choices are qualitative and the user-study statistics are outcomes, not inputs.

assumptions (4)
  • domain assumption Gestalt principles and pre-attentive processing are valid and applicable models for diagram comprehension
    Used in Section 2.1.1 to derive relative positioning, grouping, and styling operations; supported by cited literature (Koffka, Stroop, Tufte).
  • domain assumption The 58 student projects from the Forge course are representative of the diagramming needs of lightweight formal methods users
    Section 2.2 distills the language's primitives from this corpus; if the corpus is unrepresentative, the primitive set may be incomplete or skewed.
  • domain assumption The user-study scenarios (cards, subway, fruit, tic-tac-toe, face) are meaningful tests of instance understanding and bad-instance detection
    Section 5.2 constructs scenarios that avoid prior knowledge, but they are far simpler than realistic Alloy models, so results may not scale.
  • domain assumption Prolific participants with CS backgrounds are a reasonable proxy for formal methods tool users
    Section 5.2.4 acknowledges this assumption as a threat to validity; experienced Alloy users might respond differently.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Grounded Language Design for Lightweight Diagramming for Formal Methods." pith.science (2026). https://pith.science/paper/2N2KZN4V

@misc{pith2026241203310,
  author       = {Pith},
  title        = {Pith review of: Grounded Language Design for Lightweight Diagramming for Formal Methods},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2N2KZN4V}},
  note         = {Machine review of arXiv:2412.03310}
}
read the original abstract

Model finding, as embodied by SAT solvers and similar tools, is used widely, both in embedding settings and as a tool in its own right. For instance, tools like Alloy target SAT to enable users to incrementally define, explore, verify, and diagnose sophisticated specifications for a large number of complex systems. These tools critically include a visualizer that lets users graphically explore these generated models. As we show, however, default visualizers, which know nothing about the domain, are unhelpful and even actively violate presentational and cognitive principles. At the other extreme, full-blown visualizations require significant effort as well as knowledge a specifier might not possess; they can also exhibit bad failure modes (including silent failure). Instead, we need a language to capture essential domain information for lightweight diagramming. We ground our language design in both the cognitive science literature on diagrams and on a large number of example custom visualizations. This identifies the key elements of lightweight diagrams. We distill these into a small set of orthogonal primitives. We extend an Alloy-like tool to support these primitives. We evaluate the effectiveness of the produced diagrams, finding them good for reasoning. We then compare this against many other drawing languages and tools to show that this work defines a new niche that is lightweight, effective, and driven by sound principles.

Figures

Figures reproduced from arXiv: 2412.03310 by the authors.

Figure 1
Figure 1. Cope and Drag is a language built to support lightweight diagramming for lightweight formal methods. A small set of [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The Massachusetts Bay Transportation Authority (MBTA) transit map [ [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. A student-drawn diagram illustrating the layout of their spec. This layout relies on relative positioning, grouped elements, and [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (15 more)
Figure 4
Figure 4. Figure 4: Abstract syntax of Cope and Drag. P2: “We tried to start, but we had a lot of trouble figuring out how to do it [...] so we decided to focus on adding more properties to our model than spending too much time on it.” P33: “It seemed really complicated and we prefered to…
Figure 5
Figure 5. Figure 5: ring-lights Alloy Default Visualizer and CnD visualizations of a light-switching puzzle instance involving 5 lights in a ring from the Forge examples repository. Lights that are lit are colored red, while unlit lights are colored grey. (1) CnD constraints could be inte…
Figure 6
Figure 6. Figure 6: bt Alloy Default Visualizer and CnD visualizations of a binary tree. Field next cannot be laid out with directions: right, left. (2) CnD constraints could be unsatisfiable when laying out the specific instance being visualized. This is akin to a dynamic error, as it de…
Figure 7
Figure 7. Figure 7: rc Alloy Default Visualizer and CnD representations of a river-crossing puzzle instance, where a valid spec must ensure that wolves never outnumber goats on either shore. 3.3 The Lightweightness of CnD Having described how CnD is derived from the alignment of cognitive…
Figure 8
Figure 8. Figure 8: Visualizations of a binary search tree bad-instance that is a DAG. [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Visualizations of a dining-philosophers bad-instance with 6 forks and 5 philosophers. [PITH_FULL_IMAGE:figures/full_fig_p015_9.png]
Figure 10
Figure 10. Figure 10: An instance of the Filesystem specification visualized by the Alloy Default Visualizer and using [PITH_FULL_IMAGE:figures/full_fig_p017_10.png]
Figure 11
Figure 11. Figure 11: An instance of the Ring Orientation specification visualized by the Alloy Default Visualizer and using [PITH_FULL_IMAGE:figures/full_fig_p018_11.png]
Figure 12
Figure 12. Figure 12: An instance of the Chord specification visualized by the Alloy Default Visualizer and using [PITH_FULL_IMAGE:figures/full_fig_p019_12.png]
Figure 13
Figure 13. Figure 13: CnD visualizations of the scenarios described in table 1. (1) Do CnD specs help users understand the instances being explored (section 5.2.1)? (2) Can pictorial directives further enhance spec understanding (section 5.2.2 )? (3) Do CnD diagrams make salient key aspect…
Figure 14
Figure 14. Figure 14: CnD visualizations of the fruit scenario described in table 1 [PITH_FULL_IMAGE:figures/full_fig_p022_14.png]
Figure 15
Figure 15. Figure 15: The diagrams of valid and invalid Tic-Tac-Toe boards, as described in table 2. [PITH_FULL_IMAGE:figures/full_fig_p024_15.png]
Figure 16
Figure 16. Figure 16: Diagrams of valid and invalid face instances, as described in table 2. [PITH_FULL_IMAGE:figures/full_fig_p025_16.png]
Figure 17
Figure 17. Figure 17: Unexpected Penrose behaviors for a bad-instance and an instance where layout constraints are unsatisfiable. [PITH_FULL_IMAGE:figures/full_fig_p027_17.png]
Figure 18
Figure 18. Figure 18: An undirected tree specification visualized by the Alloy Default Visualizer and using [PITH_FULL_IMAGE:figures/full_fig_p030_18.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 49 canonical work pages

  1. [1]

    Greg J Badros, Alan Borning, and Peter J Stuckey. 2001. The Cassowary linear arithmetic constraint solving algorithm. ACM Transactions on Computer-Human Interaction (TOCHI) 8, 4 (2001), 267–306

    work page 2001

  2. [2]

    Leilani Battle, Danni Feng, and Kelli Webber. 2022. Exploring D3 implementation challenges on Stack Overflow. In 2022 IEEE visualization and visual analytics (VIS). IEEE, 1–5

    work page 2022

  3. [3]

    Michael Bostock, Vadim Ogievetsky, and Jeffrey Heer. 2011. D3 data-driven documents. IEEE transactions on visualization and computer graphics 17, 12 (2011), 2301–2309

    work page 2011

  4. [4]

    Hsuanwei Michelle Chen. 2017. Information visualization principles, techniques, and software. Library technology reports 53, 3 (2017), 8–16

    work page 2017

  5. [5]

    Piergiuliano Chesi. 1973. 1973 MBTA Rapid Transit Map Card. https://commons.wikimedia.org/wiki/File:1973_MBTA_rapid_transit_ map_card.jpg Public domain image

    work page 1973

  6. [6]

    Edsger W Dijkstra. 1974. Self-stabilizing systems in spite of distributed control. Commun. ACM 17, 11 (1974), 643–644

    work page 1974

  7. [7]

    Tim Dwyer. 2017. cola.js: Constraint-Based Layout in the Browser. https://ialab.it.monash.edu/webcola/ Accessed: 2024-12-02

    work page 2017

  8. [8]

    Tristan Dyer. 2024. Sterling JS Demo. https://sterling-js.github.io/demo/ Accessed: 2024-11-12

    work page 2024

Show all 52 references
  1. [9]

    Tristan Dyer and John Baugh. 2021. Sterling: A web-based visualizer for relational modeling languages. In International Conference on Rigorous State-Based Methods. Springer, 99–104

    2021

  2. [10]

    Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi. 2022. Applying cognitive principles to model-finding output: the positive value of negative information. Proceedings of the ACM on Programming Languages 6, OOPSLA1 (2022), 1–29

    2022

  3. [11]

    Robert Goldstone. 1994. An efficient method for obtaining similarity data. Behavior Research Methods, Instruments, & Computers 26 (1994), 381–386

    1994

  4. [12]

    Jane Hoffswell, Alan Borning, and Jeffrey Heer. 2018. Setcola: High-level constraints for graph layout. In Computer Graphics Forum, Vol. 37. Wiley Online Library, 537–548

    2018

  5. [13]

    Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis (2 ed.). MIT Press

    2012

  6. [14]

    Jackson and J

    D. Jackson and J. Wing. 1996. Lightweight Formal Methods. IEEE Computer (April 1996), 21–22

    1996

  7. [15]

    Kurt Koffka. 1922. Perception: an introduction to the Gestalt-Theorie. Psychological bulletin 19, 10 (1922), 531

    1922

  8. [16]

    Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, and Michael Leuschel. 2018. A Translation from Alloy to B. In Conference on Abstract State Machines, Alloy, B, and Z . 71–86. https://doi.org/10.1007/978-3-319-91271-4_6

    2018 doi

  9. [17]

    Lukas Ladenberger and Michael Leuschel. 2016. BMotionWeb: A Tool for Rapid Creation of Formal Prototypes. In Software Engineering and Formal Methods. 403–417. https://doi.org/10.1007/978-3-319-41591-8_27

    2016 doi

  10. [18]

    Jill H Larkin and Herbert A Simon. 1987. Why a diagram is (sometimes) worth ten thousand words. Cognitive science 11, 1 (1987), 65–100

    1987

  11. [19]

    Michael Leuschel and Michael Butler. 2003. ProB: A Model Checker for B. In International Symposium on Formal Methods (FM) , Keijiro Araki, Stefania Gnesi, and Dino Mandrioli (Eds.). https://doi.org/10.1007/978-3-540-45236-2_46

    2003 doi

  12. [20]

    Dor Ma’ayan, Wode Ni, Katherine Ye, Chinmay Kulkarni, and Joshua Sunshine. 2020. How domain experts create conceptual diagrams and implications for tool design. In Proceedings of the 2020 CHI Conference on Human Factors in Computing Systems . 1–14

    2020

  13. [21]

    John Maloney, Mitchel Resnick, Natalie Rusk, Brian Silverman, and Evelyn Eastmond. 2010. The scratch programming language and environment. ACM Transactions on Computing Education (TOCE) 10, 4 (2010), 1–15

    2010

  14. [22]

    Niloofar Mansoor, Hamid Bagheri, Eunsuk Kang, and Bonita Sharif. 2023. An empirical study assessing software modeling in Alloy. In 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE) . IEEE, 44–54

    2023

  15. [23]

    Lean Manual. 2024. The user-widgets system. https://lean-lang.org/lean4/doc/examples/widgets.lean.html. [Accessed Nov 19, 2024]

    2024

  16. [24]

    Vajih Montaghami and Derek Rayside. 2017. Bordeaux: A tool for thinking outside the box. In Fundamental Approaches to Software Engineering: 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, ...

    2017

  17. [25]

    Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In International Conference on Automated Deduction. Springer International Publishing, 625–635. https://doi.org/10.1007/978-3-030-79876-5_37

    2021 doi

  18. [26]

    Lekha Nair, Sujala Shetty, and Siddhanth Shetty. 2016. Interactive visual analytics on Big Data: Tableau vs D3. js. Journal of e-Learning and Knowledge Society 12, 4 (2016)

    2016

  19. [27]

    Mitchell J Nathan, Kenneth R Koedinger, Martha W Alibali, et al. 2001. Expert blind spot: When content knowledge eclipses pedagogical content knowledge. In Proceedings of the third international conference on cognitive science , Vol. 644648. 644–648

    2001

  20. [28]

    Mitchell J Nathan and Anthony Petrosino. 2003. Expert blind spot among preservice teachers. American educational research journal 40, 4 (2003), 905–928

    2003

  21. [29]

    Ayers, and Gabriel Ebner

    Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. 2023. An Extensible User Interface for Lean 4. InInteractive Theorem Proving (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 268) , Adam Naumowicz and René Thiemann (Eds.). Schloss Dagstuhl – Leibniz-Zentr...

    2023 doi

  22. [30]

    Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney LeVine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, and Shriram Krishnamurthi. 2024. Forge: A Tool and Language for Tea...

    2024

  23. [31]

    Ulrich Neumerkel and Stefan Kral. 2002. Declarative program development in Prolog with GUPU. arXiv preprint cs/0207044 (2002). Grounded Language Design for Lightweight Diagramming for Formal Methods 33

    2002 arXiv

  24. [32]

    Ulrich Neumerkel, Christoph Rettig, and Christian Schallart. 1997. Visualizing Solutions with Viewers.. In LPE. 43–50

    1997

  25. [33]

    Chris Pettitt and contributors. 2014. Dagre: A JavaScript library for directed graph layouts. https://github.com/dagrejs/dagre. Accessed: 2024-11-21

    2014

  26. [34]

    Josh Pollock, Catherine Mei, Grace Huang, Elliot Evans, Daniel Jackson, and Arvind Satyanarayan. 2024. Bluefish: Composing Diagrams with Declarative Relations. In Proceedings of the 37th Annual ACM Symposium on User Interface Software and Technology . 1–21

    2024

  27. [35]

    Helen Purchase. 1997. Which aesthetic has the greatest effect on human understanding?. In International Symposium on Graph Drawing . Springer, 248–261

    1997

  28. [36]

    Paul Shannon, Andrew Markiel, Owen Ozier, Nitin S Baliga, Jonathan T Wang, Daniel Ramage, Nada Amin, Benno Schwikowski, and Trey Ideker

  29. [37]

    Sime, Thomas R

    Max E. Sime, Thomas R. G. Green, and DJ Guest. 1977. Scope marking in computer conditionals—a psychological evaluation. International Journal of Man-Machine Studies 9, 1 (1977), 107–118

    1977

  30. [38]

    Andreas Stefik and Richard Ladner. 2017. The Quorum Programming Language (Abstract Only). In Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education (Seattle, Washington, USA) (SIGCSE ’17). Association for Computing Machinery, New York, NY, USA,

    2017

  31. [39]

    Andreas Stefik and Susanna Siebert. 2013. An empirical investigation into programming language syntax.ACM Transactions on Computing Education (TOCE) 13, 4 (2013), 1–40

    2013

  32. [40]

    Ion Stoica, Robert Morris, David Karger, M Frans Kaashoek, and Hari Balakrishnan. 2001. Chord: A scalable peer-to-peer lookup service for internet applications. ACM SIGCOMM computer communication review 31, 4 (2001), 149–160

    2001

  33. [41]

    J Ridley Stroop. 1935. Studies of interference in serial verbal reactions. Journal of experimental psychology 18, 6 (1935), 643

    1935

  34. [42]

    John Sweller and Paul Chandler. 1991. Evidence for cognitive load theory. Cognition and instruction 8, 4 (1991), 351–362

    1991

  35. [43]

    Edward R Tufte and Peter R Graves-Morris. 1983. The visual display of quantitative information . Vol. 2. Graphics press Cheshire, CT

    1983

  36. [44]

    Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi. 2018. The behavior of gradual types: a user study. ACM SIGPLAN Notices 53, 8 (2018), 1–12

    2018

  37. [45]

    Preston Tunnell Wilson, Justin Pombrio, and Shriram Krishnamurthi. 2017. Can we crowdsource language design?. In Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software . 1–17

    2017

  38. [46]

    Barbara Tversky. 2001. Spatial schemas in depictions. In Spatial schemas and abstract thought , M. Gattis (Ed.). The MIT Press, 79–112

    2001

  39. [47]

    Michelle Werth and Michael Leuschel. 2020. VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics. In Rigorous State Based Methods. 260–265. https://doi.org/10.1007/978-3-030-48077-6_21

    2020 doi

  40. [48]

    Benjamin W White. 1969. Interference in identifying attributes and attribute names. Perception & Psychophysics 6 (1969), 166–168

    1969

  41. [49]

    David Wren. 2021. animate-lean-proofs. https://github.com/dwrensha/animate-lean-proofs Accessed: 2024-11-22

    2021

  42. [50]

    Katherine Ye, Wode Ni, Max Krieger, Dor Ma’ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, and Keenan Crane. 2020. Penrose: from mathematical notation to beautiful diagrams. ACM Transactions on Graphics (TOG) 39, 4 (2020), 144–1

    2020

  43. [641]

    https://doi.org/10.1145/3017680.3022377

  44. [2003]

    Genome research 13, 11 (2003), 2498–2504

    Cytoscape: a software environment for integrated models of biomolecular interaction networks. Genome research 13, 11 (2003), 2498–2504

    2003

Pith tools

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