How do I install the Popl Writing Style skill?

Run npx skillmds@latest add brycewang-stanford/popl-writing-style in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Popl Writing Style safe to use?

This skill has not completed SkillMD's automated safety review yet. Capability flags: docs only. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Popl Writing Style?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Popl Writing Style free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Popl Writing Style?

brycewang-stanford (@brycewang-stanford) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Popl Writing Style by brycewang-stanford

Name: Popl Writing Style
Rating: 4.2 (5 reviews)
Author: brycewang-stanford

Popl Writing Style

Use when drafting or revising POPL prose — building the informal-to-formal ramp from a motivating program to definitions to a sharply stated main theorem, keeping notation coherent across 25 pages of text, writing proof sketches that name the hard case, and framing significance as an idea other PL researchers can reuse.

brycewang-stanford Updated Sep 8, 2026 1k repo stars

File contents

POPL Writing Style

A POPL paper convinces twice: informally, that the problem is real and the idea natural; formally, that the theorems are exactly true. The craft is the ramp between the two. The 25-pages-of-text budget (POPL 2027 call, read 2026-07-08) is generous compared with old conference caps — the failure mode is not compression but unmotivated formalism.

The informal-to-formal ramp

Open with a program, not a framework. Page 1 should show concrete code or a concrete derivation that misbehaves — the phenomenon your formalism explains.
State the contribution as a sharp claim. "We prove type soundness for λ_X with feature Y, the first such result without assumption Z" beats any paragraph of positioning.
Walk the example through the machinery before generalizing: the reader should predict each definition because the example demanded it.
Main theorem by the end of the overview section, at least informally: what is proved, under what assumptions, and what is not claimed.
Only then the full calculus — and every rule shown in the body should be a rule the text actually discusses (popl-supplementary takes the rest).

Notation is load-bearing

Symptom	Cost at review	Repair
Same meta-variable for terms and types	Reviewers misread a rule, file a soundness doubt	One notation table, enforced by grep
Definitions used pages before they appear	"Paper is unreadable" reviews	Definition-before-use audit on every draft
Ambient hypotheses ("we assume all contexts well-formed" once, on p. 6)	Counterexamples that your hidden assumption excludes	Number assumptions; cite by number in each theorem
Overloaded ⊢ with no annotation	Rule-reading errors in the response phase	Subscript every judgment form

Proof sketches that earn trust

A body sketch is not a shortened proof; it is a risk disclosure. Name the induction measure, name the case that fails naively, and say what saves it:

Proof sketch (Thm 4.1). By induction on the typing derivation. The interesting
case is T-Close: the naive IH is too weak because the closure captures a
context extension. We strengthen the statement to quantify over all well-formed
extensions (Lem 4.3); the remaining cases are routine and mechanized (Sound.v).

A reviewer who reads that sketch knows you met the hard case, and the appendix or mechanization confirms it.

Significance, POPL-flavored

Frame the payoff as transferable: "the proof method applies to any calculus with property P," "the logic is parametric in the memory model."
Do not oversell breadth a theorem does not have; scoping sentences ("we treat the sequential fragment; concurrency is future work") pre-empt the significance reviewer rather than arming them.
Avoid empirical-style adjectives ("fast," "practical") unless popl-experiments backs them; at this venue an unsupported "practical" is an invited objection.
Related-work sentences state technical deltas, not lists (popl-related-work).

Output format

[Ramp audit] <page where a concrete example appears / where the main claim is first stated>
[Notation risks] <overloads, forward references, ambient assumptions>
[Sketch quality] <per main theorem: hard case named? measure named?>
[Overclaim scan] <sentences claiming more than the theorems>
[Cut list] <formal material in the body that no text discusses>

---name: popl-writing-styledescription: Use when drafting or revising POPL prose — building the informal-to-formal ramp from a motivating program to definitions to a sharply stated main theorem, keeping notation coherent across 25 pages of text, writing proof sketches that name the hard case, and framing significance as an idea other PL researchers can reuse.---# POPL Writing StyleA POPL paper convinces twice: informally, that the problem is real and the ideanatural; formally, that the theorems are exactly true. The craft is the ramp betweenthe two. The 25-pages-of-text budget (POPL 2027 call, read 2026-07-08) is generouscompared with old conference caps — the failure mode is not compression but*unmotivated formalism*.## The informal-to-formal ramp1. **Open with a program, not a framework.** Page 1 should show concrete code or a concrete derivation that misbehaves — the phenomenon your formalism explains.2. **State the contribution as a sharp claim.** "We prove type soundness for λ_X with feature Y, the first such result without assumption Z" beats any paragraph of positioning.3. **Walk the example through the machinery** before generalizing: the reader should predict each definition because the example demanded it.4. **Main theorem by the end of the overview section**, at least informally: what is proved, under what assumptions, and what is *not* claimed.5. Only then the full calculus — and every rule shown in the body should be a rule the text actually discusses (`popl-supplementary` takes the rest).## Notation is load-bearing| Symptom | Cost at review | Repair ||---|---|---|| Same meta-variable for terms and types | Reviewers misread a rule, file a soundness doubt | One notation table, enforced by grep || Definitions used pages before they appear | "Paper is unreadable" reviews | Definition-before-use audit on every draft || Ambient hypotheses ("we assume all contexts well-formed" once, on p. 6) | Counterexamples that your hidden assumption excludes | Number assumptions; cite by number in each theorem || Overloaded ⊢ with no annotation | Rule-reading errors in the response phase | Subscript every judgment form |## Proof sketches that earn trustA body sketch is not a shortened proof; it is a *risk disclosure*. Name the inductionmeasure, name the case that fails naively, and say what saves it:```textProof sketch (Thm 4.1). By induction on the typing derivation. The interestingcase is T-Close: the naive IH is too weak because the closure captures acontext extension. We strengthen the statement to quantify over all well-formedextensions (Lem 4.3); the remaining cases are routine and mechanized (Sound.v).```A reviewer who reads that sketch knows you met the hard case, and the appendix ormechanization confirms it.## Significance, POPL-flavored- Frame the payoff as **transferable**: "the proof method applies to any calculus with property P," "the logic is parametric in the memory model."- Do not oversell breadth a theorem does not have; scoping sentences ("we treat the sequential fragment; concurrency is future work") pre-empt the significance reviewer rather than arming them.- Avoid empirical-style adjectives ("fast," "practical") unless `popl-experiments` backs them; at this venue an unsupported "practical" is an invited objection.- Related-work sentences state technical deltas, not lists (`popl-related-work`).## Output format```text[Ramp audit] <page where a concrete example appears / where the main claim is first stated>[Notation risks] <overloads, forward references, ambient assumptions>[Sketch quality] <per main theorem: hard case named? measure named?>[Overclaim scan] <sentences claiming more than the theorems>[Cut list] <formal material in the body that no text discusses>```

Frequently asked questions