Welcome to CGPA — Cat Girl Program Analysis! (=^.^=)
The premier online forum for cat girls who are deeply, pathologically passionate about program analysis, static analysis, formal verification, type theory, and related topics. If you found us, you're probably one of us. nya~
Note: This forum uses sensory-friendly dark mode by default. Please read the Forum Rules before posting. Neurotypicals are welcome but warned that discourse here can get very technical very fast. Don't say we didn't tell you.
The premier online forum for cat girls who are deeply, pathologically passionate about program analysis, static analysis, formal verification, type theory, and related topics. If you found us, you're probably one of us. nya~
Note: This forum uses sensory-friendly dark mode by default. Please read the Forum Rules before posting. Neurotypicals are welcome but warned that discourse here can get very technical very fast. Don't say we didn't tell you.
📊 4,821 Members
💬 128,304 Posts
📜 6,109 Threads
📅 Founded: 2019-03-14 (π day, obviously)
🆕 Newest member: QuotientTypeCat
47 users online — see who's here
Announcements & Rules
| Replies | Views | Last Post | ||
|
Please read before posting. Yes, all of it. The section on proof formatting is non-negotiable. — by Admin_TypesAllTheWayDown
Last post: LambdaWhisker
|
12replies | 8,831views |
LambdaWhisker
Today, 09:14
|
|
|
Copenhagen!! We're doing it!! Coordination thread for the official unofficial CGPA meetup. Bring your Agda proofs. — by KernelKitty
Last post: ProofPurrfection
|
58replies | 3,204views |
ProofPurrfection
Today, 11:42
|
|
Static Analysis & Abstract Interpretation
[browse all]
| Replies | Views | Last Post | ||
|
OP claims you can just do infinite iteration with lazy evaluation and it'll be fine. Everyone is extremely upset about this. nya~ — by FixpointFeline
Last post: GaloisCat — "you clearly have NOT read Cousot & Cousot 1977"
|
247replies | 14,882views |
GaloisCat
Today, 03:17
|
|
|
UPDATE: found it. it was a <= vs < in the widening operator. i hate everything. but also thank u all so much (=^.^=) — by MeownadTransformer
Last post: LatticeTabby — "we've all been there nya~"
|
89replies | 5,311views |
LatticeTabby
Yesterday, 23:58
|
|
|
Original post has 23 hand-drawn diagrams of cats representing abstraction functions and concretization functions. This is the best thread on the forum. — by AbstractKitty
Last post: NyaML — "i learned more from this than from my grad school courses"
|
156replies | 22,441views |
NyaML
2 days ago
|
|
Type Theory & Formal Verification
[browse all]
| Replies | Views | Last Post | ||
|
OP has a point but phrased it in the most incendiary way possible. 412 replies and counting. At least 3 people have linked their dissertations. One person just keeps posting ∏-types memes. — by PracticalPurr
Last post: AgdaCat — "page 27 is where it devolves into pure Agda"
|
412replies | 38,129views |
AgdaCat
Today, 07:33
|
|
|
The proof is correct. The theorem is interesting. I do not fully understand why it's true. The elaborator does though, apparently. — by WhiskerType
Last post: ProofPurrfection
|
67replies | 4,892views |
ProofPurrfection
Yesterday, 14:22
|
|
|
Mod note: this is the 8th instance of this thread. We are allowing it because the previous 7 were all archived before anyone reached a conclusion. They won't this time either. — by CubicalCat
Last post: UnivalenceFan
|
339replies | 19,003views |
UnivalenceFan
Today, 01:09
|
|
Compilers & Language Implementation
[browse all]
| Replies | Views | Last Post | ||
|
Dense. Very dense. Has an ASCII art diagram of a heap. People are arguing about whether "limited form" is the right framing. Contains some of the best technical writing on this forum. — by SepLogicKitten
Last post: PurrSec — "the bi-abduction post on page 4 is required reading"
|
198replies | 12,773views |
PurrSec
Today, 05:51
|
|
|
The syntax uses ≽^•⩊•^≼ as a valid operator. This is non-negotiable, says OP. The type system is structurally subtyped. The runtime targets WASM. — by TabbyChecker
Last post: TabbyChecker
|
45replies | 2,890views |
TabbyChecker
3 days ago
|
|
|
Discourse
LLVM vs Cranelift: The Discourse
Somehow became a thread about compile times, then register allocation theory, then someone asked about MLIR and everyone got angry. — by IRCatgirl
Last post: CatamorphismFan
|
278replies | 15,440views |
CatamorphismFan
Today, 10:00
|
|
Language Wars (Containment Zone)
[browse all]
⚠️ Mod Notice: This category exists so the rest of the forum doesn't devolve into language wars. Please keep all lang discourse here. Violations result in being quoted your own bad takes. nya~
| Replies | Views | Last Post | ||
|
The thread that never ends. Page 52 is just burrito analogies. Page 53 is people being furious about the burrito analogies. Someone on page 61 provides a correct category-theoretic explanation that everyone ignores. — by MeownadTransformer
Last post: MeownadTransformer — "(=^.^=) monads are burritos, cope"
|
523replies | 61,027views |
MeownadTransformer
Today, 12:55
|
|
|
The questions were taken anyway. SML fans showed up. F# people arrived uninvited. Someone brought up MLton. It's been three months. — by CamelCat
Last post: SMLSphynx
|
367replies | 28,512views |
SMLSphynx
Yesterday, 20:08
|
|
|
Koka fans vs Haskell fans. Someone tried to introduce Effekt and got yelled at. The thread turned into a discussion of row polymorphism and then miraculously became productive for 3 pages before relapsing. — by EffectfulKitten
Last post: RowPolyPurr
|
289replies | 17,884views |
RowPolyPurr
Today, 08:44
|
|
Off-Topic / Cat Lounge
[browse all]
| Replies | Views | Last Post | ||
|
Somehow became a thread about sensory processing. Then became a comparison spreadsheet. Then became a recommendation thread that's actually incredibly useful. — by SensoryKitten
Last post: QuietPurrgrammer
|
134replies | 9,214views |
QuietPurrgrammer
2 days ago
|
|
|
There are many photos. 'Hindley' is a grey shorthair who knocks things off tables. 'Milner' is an orange tabby who is very loud about what he wants. This tracks. — by TypeInferenceCat
Last post: CurryCat — "did you consider naming the next one 'Damas'"
|
89replies | 6,031views |
CurryCat
3 days ago
|
|
|
Strong consensus: yes. Many photos of monitors arranged in topologically interesting configurations. Someone is using a standing desk as a "sitting desk with extra steps". — by NyaML
Last post: ErgonomicPurr — "i have 4 monitors. none of them face the same direction"
|
201replies | 11,882views |
ErgonomicPurr
Yesterday, 17:39
|
|
👥 Who's Online Right Now (47 total)
NyaML, GaloisCat, MeownadTransformer, LatticeTabby, WhiskerType, AgdaCat, ProofPurrfection, PurrSec, TabbyChecker, CatamorphismFan, FixpointFeline, SepLogicKitten, CamelCat, KernelKitty, CubicalCat
... and 32 more
Most online ever: 312 users — during the PLDI 2024 live-blogging event
Most online ever: 312 users — during the PLDI 2024 live-blogging event