The best source is usually authors' websites. You can find a free copy of just about any modern CS paper by googling its title in quotes with "filetype:pdf".
None of them -- Isabelle is developed at University of Cambridge and TU Munich by academics. The parent commenter seems to have some mistaken notions and assumptions about formal methods and PL research.
You can argue that it's growing and/or promising, but there is absolutely no way that the actual research funding coming out of blockchain-land can hold a candle to the big formal methods labs at major tech firms or traditional academic research funding.
Anders Moeller and Michael Schwartzbach's book [1] on static program analysis is a fantastic resource, with (I think) a great balance of theory and practice. If you want to get really deep into the theory of program analysis, Patrick Cousot just published an incredibly thorough book on abstract interpretation (just got my copy this week, so haven't fully explored enough to have much of an opinion on it as a pedagogical resource)
No, I wouldn't say that category theory is a prerequisite for domain theory in general.
I'm most familiar with domain theory from Winskel's "Formal Semantics of Programming Languages" (great book, cited as Win93 in the linked PDF), which has a whole chapter on the subject with no reference to category theory.
If you get deeper into domain theory (e.g. by working through this book) surely some category theory will be useful, but it's not a foundational prereq.
My "wisdom" is that microeconomics is complicated... Hardly a controversial statement. I was being serious about a microecon text, but wikipedia would work just fine too.
I'm not on here to argue with people and it seems you have some sort of ideological bone to pick, so this is going to be my last reply. All the best
Sure: literally everything past the first chapter of any microeconomics textbook. Come on, your position is "it just seems obvious", so I'll just say that it _is_ obvious that economics -- a social science full of interconnected and confounding factors -- is not so simple as "if everyone has 10 more dollars then everyone's cost of living goes up by exactly 10 dollars."
Your meaning was indeed clear but I find your reasoning flawed and the cargo-cult intellectualism... silly and pretentious.
The main flaw, to me, is the 1:1 correspondence you draw between the magnitude of UBI-style benefits and cost of living. That may be true (at least under some simplified/idealized econ101 assumptions) if UBI was the sole source of money in the economy, but that's obviously not the case. The crux of the "UBI doesn't cause spiraling inflation" argument is that UBI accounts for a sufficiently small fraction of total incomes that its benefit (greater spending power for lower incomes, and the downstream economic benefits of that spending) outweighs its nonzero but noncrippling inflationary effect.
That is, though the $10 cash benefit you describe may of course increase COL, it does so by some amount between $0 and $10 that is influenced by all sorts of factors you're glossing over.
What is this gobbledygook? These technical terms have meanings that you clearly either (a) do not understand or (b) are abusing to trick less-educated folks into thinking your political opinions are authoritative and intellectual or whatever.
To an audience that _does_ speak theoretical CS, your sprinkling in of its terminology weakens whatever point you're trying to make and comes off instead as silly and pretentious.
FB uses a pretty wide array of languages internally -- I don't know if they release statistics publicly, but you can filter/search their open-source projects by language at https://opensource.fb.com/projects/#filter.
because it's not a zero sum game? those union busting talking points keep you focused on your less-fortunate colleagues and and not the obscenely wealthy guy screwing the both of you over.
For what it's worth, here are also [1] the Framework community forum thread about Arch and [2] the Arch wiki page about Framework in case you're interested.
I'm still waiting for mine to arrive (in the next batch) but I plan to install Manjaro when it does, and am cautiously optimistic that it'll be mostly painless.
Oh, thanks for the correction and apologies for the inadvertent misinfo.
Your comment sent me reading the HOPL paper about SML -- I think I (based on folklore knowledge/informal conversations) conflate the original development of ML with subsequent development and standardization around SML. All of this was well before my time so it's quite interesting to read about some of the details.
F# is an ML-family language, and ML stands for meta-language -- it was designed for language tools and compilers! Andrew Appel's Modern Compiler Implementation in ML is a great resource for code examples that aren't exactly F#, but will look damn close. The book has also been published with C and Java, if you want side-by-side comparisons
They actually dropped support for diffing and incremental parsing a few months back, when they changed up some internal structures to what they call "precise AST datatypes" (which made diffing quite tricky in the type system).
My impression (from the outside looking in) is that there weren't many people making use of those capabilities, so it wasn't a high priority feature. A bit of a shame, though -- it's a really cool tool and I enjoyed building some things on top of it. I switched to a different front-end, though, when I saw that they had removed those features and all mention of incrementality/differencing from the documentations.
I'd be happy to be wrong about this, if anyone has more up-to-date information about semantic!
The short answer is that it's unsolved in general and just done ad-hoc in practice. I'm working on incremental & demand-driven analysis techniques for my PhD research and currently building essentially what you describe. The state-of-the-art is probably this technique from this year's PLDI [1] -- last I heard they were using a batch parser but planning on integrating with tree-sitter at some point.
[1] https://dl.acm.org/doi/10.1145/3453483.3454052
adding some context: used most often in discussion of sports in my experience, e.g. Michael Jordan in Basketball, Wayne Gretzky in Hockey, Babe Ruth in Baseball, etc. Carries connotations not only of being one of the best to ever do it, but also a mythos and aura that influenced/continues to influence others.
I worked on a research project in undergrad that used Reed-Solomon -- we showed a series of images to users, who would later pick those images out of a set of un-trained images in order to authenticate or access some privileged data, sans encryption. the error-correcting allowed for some degree of misremembering or forgetfulness, as is normal in human image recognition tasks.
The professor later spun up a startup that has since been acquired by Dropbox, but I'm unaware what kind of product they're currently working on.