This is a non-negotiable foundational rule. If you are engaging in a thread about a specific paper, you must have read at least the abstract, introduction, and the section(s) being discussed. "I skimmed the title" is not sufficient. "I read a tweet about it" is grounds for mockery.

If you have not read the paper, you may ask clarifying questions, but you may not make claims about what the paper does or does not say. Violations will be corrected by other members and flagged with the tag [UNREAD]. Repeat violations will be escalated to the moderation team.

All claims referencing external work must be accompanied by a citation. The preferred format is BibTeX, enclosed in [bib]...[/bib] BBCode tags (rendered automatically). DOIs and arXiv links are also accepted. "Someone said on Twitter" is not a citation.

You may use plain author-year format (e.g., Cousot & Cousot, 1977) when BibTeX is inconvenient, but a full citation in the thread or your profile must be accessible.

↑ This is a BibTeX citation. This is what good looks like.

We are a program analysis forum. Soundness matters here. When making a formal claim, be explicit about: the semantic domain, any approximations being made, and whether your statement holds exactly or only approximately (and in which direction).

Vague hand-waving is tolerated in casual discussion threads tagged [INFORMAL], but in technical threads, imprecise claims will be challenged. Phrases like "it's basically sound" or "roughly speaking, always terminates" without qualification are considered infractions.

Relatedly: distinguish between may-analysis and must-analysis. Conflating them is a ban-worthy offense on sight (not really, but it will earn you a [PRECISION NOTICE] tag).

We recognize and accept that any sufficiently long program analysis discussion will, with probability approaching 1, drift into Haskell. This is permitted and indeed expected. However, when this happens, the poster initiating the tangent must tag their post with [OT: Haskell] in the post subject line.

Haskell tangents may include but are not limited to: monad transformer stacks for abstract interpretation, whether Data.Map.Strict is more appropriate than Data.Map.Lazy for fixpoint computation, the relationship between Foldable/Traversable and dataflow analysis, and unsolicited opinions about GHC extensions.

A dedicated subforum exists at [OT: Haskell] for extended tangents.

Program analysis has a steep learning curve. Formal methods in general can be intimidating. Everyone here was a beginner once. If someone asks a question that seems basic, answer it patiently, or link them to an appropriate resource. Do not mock, condescend, or post "did you even read Nielson et al." without also telling them what Nielson et al. is.

The Beginner's Corner subforum exists for introductory questions. Redirect new members there if appropriate, but do so gently and helpfully, not dismissively.

Members with the [NEWBIE] flair are especially protected by this rule. Moderation team will act swiftly on reports of beginner-shaming.

This is a forum tradition that has hardened into rule. The user GaloisCat has, through years of meticulous posting, earned the designation of Resident Galois Connection Authority. When GaloisCat makes a claim about Galois connections, the adjoint functor theorem, or related order-theoretic constructions, the burden of proof for disagreement is elevated.

This does not mean GaloisCat is infallible — they have been wrong before (the Great Galois Connection Incident of 2023 is documented in the archive). It means you should have a solid, cited argument before claiming they are wrong. "I think you're wrong" with no proof will be disregarded and the thread will move on.

GaloisCat has accepted this responsibility with characteristic humility and occasional nya~s.

The topic of widening operators — their design, their selection, their application, and most especially their effectiveness vs. precision tradeoffs — is a known flashpoint on this forum. Threads which the OP anticipates will involve heated debate about widening must be tagged [FLAME WAR] in the title.

Widening-adjacent topics that frequently escalate and therefore also require the tag include: delay widening vs. standard widening, semantic widening, the PAGAI paper, anything related to the -∞ widening convention, and the perennial "is widening even necessary if you just pick the right abstract domain" debate.

Threads that become a flame war without prior tagging will be retroactively tagged by a moderator and the OP will receive a gentle nudge. Second offense within 30 days incurs a 48-hour cooldown from the Static Analysis subforum.

The posting of ASCII cat art in threads, signatures, and profile pages is actively encouraged. This is a cultural cornerstone of CGPA and has been since the forum's founding. Original cat art is especially valued. Cats in the style of formal notation (e.g., a cat depicted using λ-calculus symbols, or a cat drawn with lattice-theoretic characters like ⊓ and ⊔) earn extra community respect.

The ASCII Gallery subforum exists for showcasing and archiving notable contributions. The annual Best ASCII Cat Art Award (🏆 BestMeow) is awarded by community vote each December.

The use of nya~ (and variants: nya, nyaa~, nyan, (=^･ω･^=), etc.) in posts and thread closings is completely optional and will never be required, penalized, or mocked. It is, however, appreciated by a significant portion of the community and considered a warm, friendly gesture.

If you are uncomfortable with cat affectations, that is entirely valid — CGPA is first and foremost a technical forum, and rigorous program analysis discussion stands on its own merits. The nya~ culture is opt-in and non-coercive.

Members who use nya~ may optionally display the [=^ω^=] flair on their profile. See Profile Settings to enable this.

nya~ — CatModerator (demonstrating by example)

This forum is powered by Rabbithole, an AI web page generator. Members are permitted to post content generated or assisted by Rabbithole or other AI systems, subject to the following conditions:

1. All AI-generated or AI-assisted content must be tagged with [AI: Rabbithole] or [AI: <system name>] at the top of the post.
2. The poster is personally responsible for verifying the accuracy of AI-generated claims. Rule 3 (No Unsound Approximations) applies with increased scrutiny to AI-generated content.
3. AI-generated BibTeX citations must be independently verified before posting. AI systems hallucinate citations. Do not post a fake Cousot paper.
4. The community reserves the right to [UNVERIFIED]-tag any AI content that appears incorrect or fabricated.

Using Rabbithole to generate ASCII cat art is not only allowed but delightful. Using it to fabricate paper summaries you have not read violates Rule 1 as well as this rule. nya~