Pith. sign in

REVIEW 1 major objections 6 minor 34 references

Pantograph: A Fluid and Typed Structure Editor

T0 review · 1 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read By generalizing selection to one-hole contexts and typing edits with diffs, a structure editor can stay well-formed and well-typed at every moment without sacrificing fluidity.

desk verdict A genuinely new and mostly solid structure-editing paper whose main formal gap is an under-specified unification step in the generic propagation rules, leaving the confluence claim slightly loose as written. read the letter →

arxiv 2411.16571 v2 pith:JDPI7IJG submitted 2024-11-25 cs.PL

Jacob Prinz , Henry Blanchette , Leonidas Lampropoulos This is my paper · ORCID
classification cs.PL MSC 68N3068Q4203B70
keywords structureeditorszippereditingone-holecontextstypediffsdiffpropagationpreservationconfluenceviscosity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper argues that the viscosity problem of structure editors is solvable: an editor can keep every program state syntactically well-formed and well-typed while still letting users freely rearrange code the way text editors do. The key is to generalize text selection to trees as one-hole contexts, so selecting and editing what lies between two tree cursors becomes a single cut-and-paste operation. To keep edits well-typed in addition to well-formed, the paper types each one-hole context by a diff between its inner and outer types, and propagates that diff through the surrounding program with a small-step rewriting system, automatically updating type annotations, inserting arguments, or placing first-class error forms where needed. The formal claims are progress, type preservation, termination, and confluence for this propagation system, proved for a small simply-typed core language.

What carries the argument

The central objects are one-hole contexts and type diffs. A one-hole context $C[\cdot]$ is a tree with a single missing subterm; generalizing text selection to trees means selecting, cutting, and pasting an arrangement $C_1[C_2[t]]$, i.e., the program decomposed into two contexts and a focus term. Type diffs $\delta$ describe how a type changes across an edit, with constructors for identity, childwise change, adding or removing a function argument, and replacement; they form a category under composition. Diff boundaries $\{t\}^{\uparrow}_{\Delta \vdash \delta}$ and $\{t\}^{\downarrow}_{\Delta \vdash \delta}$, carrying diffs for both the typing context and the type, are propagated through terms by rules derived from intrinsic typing rules via diff substitutions over metavariables. The eight alteration rules (insert/delete abstraction, insert/displace/delete application, local-to-free and free-to-local) make the actual code changes, and error boundaries $\{t\}^{!}$ abort propagation when no other rule applies.

What would settle it

Run the propagation system on reachable edit states in the implemented core calculus and search for a term that contains a diff boundary not at the top to which no rewrite rule applies; any such stuck state falsifies the Progress theorem, and two different terminal terms from one edit state falsify confluence. A ready target is a language extension with a polymorphic typing rule in which a type variable appears twice in a premise, where the paper's linearity-based invariants are known to be delicate.

Watch

Extended reading notes

Core claim

The paper's central discovery is that the viscosity problem of structure editors is not fundamental: a selection mechanism based on one-hole contexts supports the same cut-and-paste fluidity as text editing while preserving well-formedness, and typing those contexts with a category of diffs extends the guarantee to well-typedness. A user edit to the program (inserting, removing, or altering a one-hole context) is represented as a diff boundary, an internal term-shaped marker carrying a context diff and a type diff; a small-step rewriting system then propagates the boundary through the program by matching each language construct's typing rule, and eight hard-coded alteration rules decide how to update the surrounding code, inserting lambdas or applications, displacing arguments into commented applications, converting bound variables to free ones, or wrapping an offending subterm in a first-class type error boundary. The propagation system is proved terminating, type-preserving, confluent, and total (progress).

Load-bearing premise

The formal guarantees are proved only for a small simply-typed core language with integers, booleans, functions, lists, and pattern matching, and the paper assumes the same typed-diff propagation works in full languages with polymorphism, dependent types, or effects.

Editorial extensions

If this is right

  • Restructuring edits such as adding a parameter to a function become a single cut-and-paste operation, with the system automatically updating the type signature, call sites, and recursive calls.
  • An editor built on this scheme never needs to re-parse or re-typecheck the program after an edit, since each state is well-formed and well-typed by construction.
  • Type errors become first-class, user-editable forms (free variables, commented applications, and error boundaries) that can be selected and deleted like any other construct.
  • The diff category gives edit sequences a compositional semantics: two consecutive edits compose into a single diff, which is the basis for undo/redo and for reasoning about refactorings.

Reading between the lines

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

  • Nothing in the proof prevents the same machinery from being used outside an editor, for example as a refactoring engine for typed ASTs where a program transformation is specified as a diff and then propagated; the paper does not explore this direction.
  • A natural stress test is polymorphic recursion: the confluence invariant relies on at most one up-like boundary at a time, and it is unclear whether this survives language features with nonlinear typing rules beyond the core calculus.
  • The user study compares only against a text editor and reports roughly 1.4x slower average task time; a direct comparison with gradual structure editors that allow grammar-breaking edits, which the paper does not run, would separate the cost of typed diff propagation from the cost of tree-based interaction.
  • Multi-hole selections (cutting two disjoint subtrees at once) might remove the remaining multiplicity barriers that the paper lists as limitations; this is a concrete interface extension the authors do not implement.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 6 minor

Summary. The paper presents Pantograph, a structure editor that generalizes text selection to tree-based one-hole contexts ("zipper editing") and uses this abstraction to maintain syntactic well-formedness of programs at every edit. To additionally preserve well-typedness, the paper introduces a category of type diffs: each one-hole context is assigned a diff that describes how the type and typing context change when that context is inserted or removed. The main formal device is a small-step diff-propagation system that carries diff boundaries through a simply-typed core calculus with integers, booleans, functions, lists, pattern matching, typed holes, and three explicit error forms (free variables, commented applications, and type-error boundaries). The paper claims Theorems 3--6 for this system: Progress, Type Preservation, Termination, and Confluence, with proofs in Appendices B and C. It also reports on an implementation of Pantograph and a user study with 13 students, finding that participants could learn to use the editor and solve tasks, though they were on average slower than with a text editor. The final sections discuss limitations and related work.

Significance. The central idea of the paper---generalizing text selection to one-hole contexts and typing those contexts with a category of diffs---is a genuine and non-obvious contribution to the structure-editor literature, and it is developed with unusual care. The formal development is largely self-contained: diffs are defined from scratch, the category laws for diffs are proved, and the small-step system is shown to preserve types and terminate. The paper is also honest about scope: the metatheory is for the small simply-typed core of Figure 6, and the user study is presented as a feasibility study with explicit limitations. An artifact is available, which strengthens the empirical claims. If the formal system is fully pinned down, this is a solid POPL contribution; the main barrier to acceptance is the underspecification of the generic propagation rules discussed in the major comments.

major comments (1)
  1. [§5.6, Theorem 3 proof] The treatment of the final top-level up boundary is not fully specified. The proof of Theorem 3 says that if the final program has the form {t}↑_{Δ⊢δ}, an invariant shows Δ = id and "Pantograph removes the boundary and the program has a new type." However, no small-step rule removes a non-identity up boundary (Identity↑ requires δ = id), and removing such a boundary changes the type of the program, which would conflict with the statement of Theorem 4 if the removal is considered a step of the relation. Please clarify whether the removal is part of the rewrite relation or an external "commit" operation, and state how Type Preservation is meant to account for the resulting type change.
minor comments (6)
  1. [Appendix B.3, Lemma 6] The statement of Lemma 6 refers to a neutral form u, but the case analysis inside the proof uses t instead of u; aligning the notation would avoid confusion.
  2. [§5.5, Insert-App↑] The rule as written in the main text uses t on the left and t in the output, while the neighboring Displace-App↑ and the appendix rule use t1 and t2; please make the metavariable usage uniform across the two presentations.
  3. [§6.1] The treatment of omitted participants and discarded data points is described in prose but would benefit from a small table listing per-participant task counts, skipped tasks, and which data points were discarded, to make the reported 124 data points easy to verify.
  4. [§6.2] The sentence "All but two participants made use of the diff propagation to solve the problem - one manually rewrote a function call instead, and the other skipped the problem" gives numbers for 13 participants, but the analysis earlier in the section is based on 11 participants; please reconcile these counts explicitly.
  5. [§3] The grammar of type diffs introduces +⟨T→⟨δ⟩⟩ and −⟨T→⟨δ⟩⟩, while Section 5.2 generalizes these to +⟨c⟨d⟩⟩ and −⟨c⟨d⟩⟩; a short sentence explaining that the earlier T→⟨δ⟩ is the specialization of the one-hole context c to a function type would help readers connect the two presentations.
  6. [§5.6] The paper states the formal theorems for the core calculus of Figure 6 and acknowledges in Section 7 that the full language is not covered; a closing sentence in Section 9 noting that extension to features such as polymorphism, effects, and dependent types remains open would match the paper's otherwise careful limitations statement.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the formal metatheory is self-contained and the only self-citation is not load-bearing.

full rationale

The paper's central formal claims (Progress, Type Preservation, Termination, Confluence in Theorems 3-6) are proved from definitions introduced in the paper itself: the category of type/context diffs (Section 5.2), typing of one-hole contexts (Section 5.3), and the propagation/alteration/diff-boundary rules (Sections 5.4-5.5). These definitions are not fitted to data, and no predicted quantity is statistically forced by a fitted parameter. The only self-citation is the artifact DOI for reproducibility, which is not load-bearing for any theorem. The user study makes no predictive claim that could reduce by construction; its limitations, including potential experimenter bias, are explicitly acknowledged in Section 6.3. Section 7 candidly states limitations of the zipper and typed editing paradigms. The skeptic's point about Section 5.4 is real but is an under-specification/correctness risk: the generic Propagate rules rely on an existential decomposition `s = C[s']` with a diff substitution `sigma`, and the paper does not prove uniqueness or give a canonical unification procedure. That leaves the rewrite relation incompletely pinned down, but it does not make any claimed result equivalent to its own inputs by definition. No quoted step exhibits the required reduction, so the appropriate finding is no significant circularity.

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

The central formal claims rest on the core calculus and the hard-coded alteration rules; no numerical free parameters are fitted. The system's breadth beyond the core language is assumed rather than proved, and the user-study findings depend on assumptions about task representativeness and participant behavior that the paper explicitly acknowledges.

assumptions (4)
  • domain assumption The standard typing rules for the core language in Figure 6 define well-typedness, and the metatheory holds relative to this calculus.
    Type preservation, progress, termination and confluence are proved for this specific calculus, not for a full language with polymorphism, dependent types, or effects.
  • domain assumption One-hole-context selection is a faithful generalization of text selection and cut-and-paste.
    Section 2 defines selection as C1[C2[t]] and uses this to claim fluidity, but the paper itself notes limitations such as multiplicity and difficulties with some imperative or HTML-like edits in Sections 7 and 8.
  • ad hoc to paper The eight alteration rules in Section 5.5 are an adequate design for automatic typed edits.
    These rules are hard-coded design choices, not derived from first principles; their completeness for all desirable edits is not proved, only demonstrated through examples.
  • standard math Standard mathematical results used in the proofs: Newman's lemma for confluence and the Dershowitz-Manna multiset ordering for termination.
    These are cited and applied in Appendix B.1 and B.3 without proof, which is normal for a POPL paper.
invented entities (3)
  • Type diffs (category of diffs over trees) independent evidence
    purpose: Type one-hole contexts and propagate type changes through the program when an edit is made.
    The diff formalism is implemented in the Pantograph editor and exercised in the user study; it has a concrete artifact, although it is not a physical entity with external falsifiable predictions.
  • Diff boundaries (up and down boundaries, {t}^up and {t}^down) independent evidence
    purpose: Represent intermediate states during diff propagation through the program.
    These are internal to the propagation algorithm and are implemented in the editor; their behavior is specified by the small-step rules.
  • Free variables, commented applications, and type error boundaries as first-class error forms independent evidence
    purpose: Allow an otherwise well-typed program to contain unresolved edits without resorting to untyped syntax.
    These constructs have typing rules, appear in the implementation, and are interactively manipulable in Pantograph, as shown in the examples in Section 3.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Pantograph: A Fluid and Typed Structure Editor." pith.science (2026). https://pith.science/paper/JDPI7IJG

@misc{pith2026241116571,
  author       = {Pith},
  title        = {Pith review of: Pantograph: A Fluid and Typed Structure Editor},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JDPI7IJG}},
  note         = {Machine review of arXiv:2411.16571}
}
read the original abstract

Structure editors operate directly on a program's syntactic tree structure. At first glance, this allows for the exciting possibility that such an editor could enforce correctness properties: programs could be well-formed and sometimes even well-typed by construction. Unfortunately, traditional approaches to structure editing that attempt to rigidly enforce these properties face a seemingly fundamental problem, known in the literature as viscosity. Making changes to existing programs often requires temporarily breaking program structure -- but disallowing such changes makes it difficult to edit programs! In this paper, we present a scheme for structure editing which always maintains a valid program structure without sacrificing the fluidity necessary to freely edit programs. Two key pieces help solve this puzzle: first, we develop a novel generalization of selection for tree-based structures that properly generalizes text-based selection and editing, allowing users to freely rearrange pieces of code by cutting and pasting one-hole contexts; second, we type these one-hole contexts with a category of type diffs and explore the metatheory of the system that arises for maintaining well-typedness systematically. We implement our approach as an editor called Pantograph, and we conduct a study in which we successfully taught students to program with Pantograph and compare their performance against a traditional text editor.

Figures

Figures reproduced from arXiv: 2411.16571 by the authors.

Figure 1
Figure 1. Structured vs Text Editing Example In this manner one can fill in the entire program, and never be permitted to make a syntax or type error. Unsurprisingly, this quite rigid approach very quickly breaks down: how can one edit existing code? Suppose that the programmer realizes that l2 never contains negative numbers, and decides to optimize the expression by moving the execution of the append operation to after the … view at source ↗
Figure 2
Figure 2. Text- and Tree-based Cursors and Selection [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Inserting a λ around a term of the program: Users query the name of the construction that they want to insert, and Pantograph wraps it around the term at the cursor; ?0 represents an unknown type. For concreteness, consider the following simple functional language core, consisting of 𝜆 abstrac￾tions, applications, variables, let expressions, and term holes. 𝑡 ::= let 𝑥 : 𝑇 = 𝑡 in 𝑡 | λ𝑥 : 𝑇 . 𝑡 | 𝑡 𝑡 | 𝑥 𝐶 ::= let 𝑥… view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Cutting and pasting a selection into a different location in Pantograph. Zipper editing lends itself to [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Various edits each performed with a single cut and paste of a one-hole context selection. The first [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: A typed core language 3 Typed Editing Zipper editing, like the traditional structure editing it extends, preserves the syntactic well￾formedness of programs. However, it does not necessarily preserve well-typedness. Let’s add a few types to our core language of the pre…
Figure 7
Figure 7. Figure 7: Typed editing example 1: adding a parameter to map [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]
Figure 8
Figure 8. Figure 8: Typed editing example 2: adding a higher-order parameter to map [PITH_FULL_IMAGE:figures/full_fig_p009_8.png]
Figure 9
Figure 9. Figure 9: Typed editing example 3: deleting a parameter. This deletion requires updating the rest the program [PITH_FULL_IMAGE:figures/full_fig_p009_9.png]
Figure 10
Figure 10. Figure 10: Typed editing example 4: replacing one type with another. The corresponding type diff for this edit [PITH_FULL_IMAGE:figures/full_fig_p010_10.png]
Figure 11
Figure 11. Figure 11: Typed editing example 5: deleting a type error boundary. When the user deletes the type boundary, [PITH_FULL_IMAGE:figures/full_fig_p011_11.png]
Figure 12
Figure 12. Figure 12: Task durations (in seconds) split by editor. For each task, Pantograph times are on the top in orange, [PITH_FULL_IMAGE:figures/full_fig_p022_12.png]
Figure 13
Figure 13. Figure 13: Geometric mean and variance of relative task times for each participant (denoted as a dot), and for [PITH_FULL_IMAGE:figures/full_fig_p022_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 13 canonical work pages

  1. [3]

    1⟨𝑑′ 1⟩⟩,𝑑2 =𝑐[𝑑′ 2], and𝑑3 =𝑐[𝑑′ 3] •( +⟨𝑐

    (8) If 𝑑1 =+⟨𝑐. 1⟨𝑑′ 1⟩⟩,𝑑2 =𝑐[𝑑′ 2], and𝑑3 =𝑐[𝑑′ 3] •( +⟨𝑐. 1⟨𝑑′ 1⟩⟩◦ 𝑐[𝑑′ 2])◦ 𝑐[𝑑′ 3] =+⟨𝑐. 1⟨𝑑′ 1◦𝑑′ 2⟩⟩◦ 𝑐[𝑑′ 3] =+⟨𝑐. 2⟨(𝑑′ 1◦𝑑′ 2)◦ 𝑑′ 3⟩⟩ • +⟨𝑐. 1⟨𝑑′ 1⟩⟩◦( 𝑐[𝑑′ 2]◦ 𝑐[𝑑′ 3]) =+⟨𝑐. 1⟨𝑑′ 1⟩⟩◦ 𝑐[𝑑′ 2◦𝑑′ 3] =+⟨𝑐. 2⟨𝑑′ 1◦(𝑑′ 2◦𝑑′ 3)⟩⟩ (9) If 𝑑1 =𝑐1[𝑑′ 1],𝑑2 =𝑐2[𝑑′ 2], and𝑑3 =−⟨𝑐2.2⟨𝑑′ 3⟩⟩ •( 𝑐1[𝑑′ 1]◦ 𝑐2.2[𝑑′ 2])◦ −⟨𝑐. 2⟨𝑑′ 3⟩⟩ =(𝑐1◦𝑐2)[𝑑′ 1◦𝑑′ 2]◦ −⟨𝑐...

    work page 2024

  2. [12]

    IEEE Transactions on Software Engineering 38, 1 (Jan

    GenProg: A Generic Method for Automatic Software Repair. IEEE Transactions on Software Engineering 38, 1 (Jan. 2012), 54–72. https://doi.org/10.1109/tse.2011.104 C. Le Goues, M. Pradel, A. Roychoudhury, and S. Chandra

    doi:10.1109/tse.2011.104 2012

  3. [13]

    IEEE Software 38, 04 (jul 2021), 22–27

    Automatic Program Repair. IEEE Software 38, 04 (jul 2021), 22–27. https://doi.org/10.1109/MS.2021.3072577 Eyal Lotem and Yair Chuchem

    arXiv 2021

  4. [15]

    (01 2010)

    Ornamental algebras, algebraic ornaments. (01 2010). https://personal.cis.strath.ac.uk/conor.mcbride/ pub/OAAO/LitOrn.pdf John McCarthy

    work page 2010

  5. [21]

    Live functional programming with typed holes. Proc. ACM Program. Lang. 3, POPL, Article 14 (jan 2019), 32 pages. https://doi.org/10.1145/3290327 Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer

    doi:10.1145/3290327 2019

  6. [24]

    Springer Berlin Heidelberg, 1–16

    Constraint-Free Type Error Slicing. Springer Berlin Heidelberg, 1–16. https://doi.org/10.1007/978-3- 642-32037-8_1 Jeremy Siek and Walid Taha

    doi:10.1007/978-3-

  7. [28]

    Publication date: January 2025

    2025

  8. [29]

    Proceedings of the ACM on Programming Languages 2, POPL (Dec

    A principled approach to ornamentation in ML. Proceedings of the ACM on Programming Languages 2, POPL (Dec. 2017), 1–30. https://doi.org/10.1145/3158109 Eric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, and Cyrus Omar

    work page doi:10.1145/3158109 2017

Show all 34 references
  1. [30]

    Proceedings of the ACM on Programming Languages 8, POPL (Jan

    Total Type Error Localization and Recovery with Holes. Proceedings of the ACM on Programming Languages 8, POPL (Jan. 2024), 2041–2068. https: //doi.org/10.1145/3632910 Proc. ACM Program. Lang., Vol. 9, No. POPL, Article

    2024 doi

  2. [31]

    We construct an ordering over the set of all of the diff boundaries within the program

    Pantograph: A Fluid and Typed Structure Editor 28:35 order to prove termination of our algorithm. We construct an ordering over the set of all of the diff boundaries within the program. We use a Dershowitz-Manna ordering [Dershowitz and Manna 1979]. In this ordering, if𝑆1 and𝑆...

    1979

  3. [32]

    In this state, again, either boundary can be stepped next

    28:38 Jacob Prinz, Henry Blanchette, and Leonidas Lampropoulos let𝑓 :(Int→ Bool)→ Int = λ𝑥 : Int→ Bool .{{𝑥}↑ 𝑖𝑑⊢Int→( Int/ Bool) 10}↓ 𝑓 :(Int/ Bool)→Int,𝑥:𝑖𝑑⊢𝑖𝑑 in ... In this state, again, either boundary can be stepped next. But in this case the Interchange rules will apply...

    1942

  4. [1942]

    Equivalence

    On Theories with a Combinatorial Definition of "Equivalence". Annals of Mathematics 43, 2 (1942), 223–243. http://www.jstor.org/stable/1968867 Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer

    1942

  5. [1960]

    Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (apr 1960), 184–195. https://doi.org/10.1145/367177.367199 Microsoft

    1960

  6. [1972]

    Indagationes Mathematicae (Proceedings) 75, 5 (1972), 381–392

    Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75, 5 (1972), 381–392. https: //doi.org/10.1016/1385-7258(72)90034-0 Nicola Dell, Vidya Vaidyanatha...

    1972 doi

  7. [1979]

    Proving termination with multiset orderings. Commun. ACM 22, 8 (Aug. 1979), 465–476. https://doi.org/10.1145/359138.359142 Jana Dunfield and Neel Krishnaswami

    1979

  8. [1986]

    In Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL ’86 (POPL ’86)

    Finding the source of type errors. In Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL ’86 (POPL ’86) . ACM Press. https://doi.org/10.1145/512644.512648 Thomas Williams and Didier Rémy

  9. [1995]

    (03 1995)

    The Implementation of ALF - a Proof Editor based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution. (03 1995). Thomas Schilling

    1995

  10. [1997]

    The Zipper. J. Funct. Program. 7, 5 (sep 1997), 549–554. https://doi.org/10.1017/S0956796897002864 Amy J. Ko, Htet Htet Aung, and Brad A. Myers

    1997 doi

  11. [2001]

    ACM Transactions on Software Engineering and Methodology 10, 1 (Jan

    A slicing-based approach for locating type errors. ACM Transactions on Software Engineering and Methodology 10, 1 (Jan. 2001), 5–55. https://doi.org/10.1145/366378.366379 Markus Voelter

    2001

  12. [2003]

    In HCI Models, Theories, and Frameworks , John M

    CHAPTER 5 - Notational Systems—The Cognitive Dimensions of Notations Framework. In HCI Models, Theories, and Frameworks , John M. Carroll (Ed.). Morgan Kaufmann, San Francisco, 103–133. https://doi.org/10.1016/B978-155860808-5/50005-8 Henry Blanchette and Jacob Prinz

    doi

  13. [2005]

    In CHI ’05 Extended Abstracts on Human Factors in Computing Systems (CHI05)

    Design requirements for more flexible structured editors from a study of programmers’ text editing. In CHI ’05 Extended Abstracts on Human Factors in Computing Systems (CHI05) . ACM. https://doi.org/10.1145/1056808.1056965 Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, an...

  14. [2006]

    Qualita- tive Research in Psychology 3, 2 (2006), 77–101

    Using thematic analysis in psychology. Qualita- tive Research in Psychology 3, 2 (2006), 77–101. https://doi.org/10.1191/1478088706qp063oa arXiv:https://www.tandfonline.com/doi/pdf/10.1191/1478088706qp063oa Virginia Braun and Victoria Clarke

    2006 doi

  15. [2010]

    ACM Trans

    The Scratch Programming Language and Environment. ACM Trans. Comput. Educ. 10, 4, Article 16 (nov 2010), 15 pages. https://doi.org/10.1145/ 1868358.1868363 Conor McBride

    2010

  16. [2012]

    Yours is better!

    “Yours is better!”: participant response bias in HCI. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (CHI ’12) . ACM. https://doi.org/10.1145/2207676.2208589 Nachum Dershowitz and Zohar Manna

  17. [2013]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 383–430

    Language and IDE Modularization and Composition with MPS . Springer Berlin Heidelberg, Berlin, Heidelberg, 383–430. https://doi.org/10.1007/978-3-642-35992-7_11 Markus Voelter, Janet Siegmund, Thorsten Berger, and Bernd Kolb

    doi

  18. [2015]

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik

    Refined Criteria for Gradual Typing. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SNAPL.2015.274 F. Tip and T. B. Dinesh

    2015 doi

  19. [2016]

    In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (Seattle, WA, USA) (FSE 2016)

    Efficiency of projectional editing: a controlled experiment. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (Seattle, WA, USA) (FSE 2016). Association for Computing Machinery, New York, NY, USA, 763–774. https://doi.o...

    2016

  20. [2017]

    In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17)

    Hazelnut: a bidirectionally typed structure editor calculus. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17) . Association for Computing Machinery, New York, NY, USA, 86–99. https: //doi.org/10.1145/3009837.300...

  21. [2019]

    Qualitative Re- search in Sport, Exercise and Health 11, 4 (2019), 589–597

    Reflecting on reflexive thematic analysis. Qualitative Re- search in Sport, Exercise and Health 11, 4 (2019), 589–597. https://doi.org/10.1080/2159676X.2019.1628806 arXiv:https://doi.org/10.1080/2159676X.2019.1628806 Adam Chen, Thomas Porter, and Cyrus Omar

    2019

  22. [2021]

    ACM Comput

    Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (may 2021), 38 pages. https://doi.org/10.1145/3450952 Future of Programming Lab

    2021 doi

  23. [2022]

    In Proceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development (Ljubljana, Slovenia) (TyDe 2022)

    tylr: a tiny tile-based structure editor. In Proceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development (Ljubljana, Slovenia) (TyDe 2022). Association for Proc. ACM Program. Lang., Vol. 9, No. POPL, Article

    2022

  24. [2023]

    In 2023 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC)

    Gradual Structure Editing with Obligations. In 2023 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC) . IEEE. https://doi.org/10.1109/vl-hcc57772.2023.00016 M. H. A. Newman

    2023

  25. [2024]

    https://doi.org/10.5281/zenodo.14199877 Virginia Braun and Victoria Clarke

    Pantograph Implementation. https://doi.org/10.5281/zenodo.14199877 Virginia Braun and Victoria Clarke

    doi

  26. [2025]

    https://doi.org/10.1145/3546196.3550164 David Moon, Andrew Blinn, and Cyrus Omar

    28:30 Jacob Prinz, Henry Blanchette, and Leonidas Lampropoulos Computing Machinery, New York, NY, USA, 28–37. https://doi.org/10.1145/3546196.3550164 David Moon, Andrew Blinn, and Cyrus Omar

Pith tools

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