Pinned toot

"Combines the constructivism of intuitionist logic with the duality of classical logic" sounds interesting. Wish I could read

Show thread

I found sequent calculus rules online, but I do not understand them. They don't seem like the usual format that typing rules have. I can't really wrap my head around what they're supposed to mean

Show thread

Does anyone know of like an "informal" explanation of linear logic?

me if I were a commutative diagram: (commutes)

I wonder if HoTT "scales" to like, analysis and whatnot

Show thread

If you pick up any math book and try to translate a proof into a proof assistant, it's not just tedious, it's hard. Unless you happen to pick up HoTT, I guess, and you happen to be using a proof assistant based on constructive type theory

Get it. Do you get it. It's cause small step semantics, big step semantics. Do you get it

Show thread

One small step for theory, one big step for implementation

If Coq had Isar, and rewrite rules, that would be like, awesome

I would not refute LEM. I would instead prefer to have a rule which all agreed was intuitive and obviously true, which nonetheless refuted LEM

I am like copy, paste, s/blast/iprover, "I am like a mathematician now, probably"

Show thread

I also hooked up Isabelle's case splitter and induction tactics, but it's anyone's guess whether these actually work cause they rely on classical theorems, and I just lied instead and fed it contrapositivity

Show thread

For unknown reasons, I have hooked up Isabelle/IFOL to Isabelle's simplifier and plonked on a constructivized version of HOL's set theory (I replaced "by blast" with "by iprover" and removed some classical lemmas which were unprovable)

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.