#curryhoward — Public Fediverse posts

From 11:00 to 12:00 on Thursday, May 28, the PLUSLE reading group will discuss "Proofs as Processes" by Samson Abramsky, as well as the first two sections of "Propositions as sessions" by Philip Wadler.

https://plsl.acp.sdu.dk/posts/2025-05-28-proofs-as-processes-propositions-as-sessions/

#PLUSLE #curryHoward #propositionsAsTypes #concurrency #logic #lambdaCalculus #piCalculus #programmingLanguages #functionalProgramming

🎉🎩 Welcome to the 32-minute saga of "How to Pretend You're a Genius by Confusing #Rust and Everyone Else." Spoiler: it involves emulating HKTs, crashing #compilers, and invoking Curry-Howard theories just to sound smart. 🚀💥 Pro tip: when your argument starts resembling a mathematical fever dream, it’s time to reevaluate your life choices. 🤦‍♂️
https://www.harudagondi.space/blog/torturing-rustc-by-emulating-hkts/ #PretendGenius #CurryHoward #TechHumor #CodingLife #HackerNews #ngated

Not withstanding #CurryHoward (propositions are types, proofs are values), typical IT coders (even the skilled non-vibers) today can no longer read and do proofs. Most coders in the industry are not even aware that mathematics is at the foundation of computing. A few who are aware invariably throw up this trite defence: modern IT has evolved beyond that ancient notion of “#programming is a #mathematical activity”.

That “maths is superfluous to coding” argument is as fallacious as proposing to sack all airline transport pilots because modern airliners can now takeoff, cruise, and land automatically, or calling to defrock all mathematicians because there are now proof assistants, like Agda and Lean.

Latin is no longer the lingua franca, but classics students still learn this so-called dead language. Pilots no longer need to hand fly airliners, but they still maintain their stick-and-rudder currency. The undergraduate maths curriculum is now automated in Lean (see Buzzard), but every maths undie can still whip out paper proofs, on demand. Likewise, programmers no longer rely on proofs in their daily work, but they should still hone this essential skill—because it is good for the mind.

Ok this was generated by googles gemini image generator and I quiet like it :)

#fp #lambda #CurryHoward #turing #gödel #church

Readings shared August 24, 2024. https://jaalonso.github.io/vestigium/posts/2024/08/25-readings_shared_08-24-24 #Logic #Racket #ITP #Coq #Agda #TypeTheory #CurryHoward

Tipos dependientes: λP. ~ Juan Pablo Yamamoto Zazueta. https://jpyamamoto.com/projects/dependent-types/dept.pdf #TypeTheory #CurryHoward

Lecturas compartidas el 5 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/06-lecturas_compartidas_el_05-ago-24 #ATP #SAT #Haskell #FunctionalProgramming #CurryHoward #TypeScript

Proofs are programs: A few examples of the Curry-Howard correspondence. ~ Adam Dueck. https://adueck.github.io/blog/curry-howard-proofs-are-programs/ #CurryHoward #TypeScript

By #CurryHoward isomorphism, types are propositions and programmes are proofs. So, those who write programmes are proof writers. That is, a #programmer's job is exactly like a #mathematician's job—assiduous, persistent, audacious, creative, ingenuous.

A working mathematician simply cannot cut and paste published proofs and call it his work product; he must propel the field forward. Yet, working programmers satisfy themselves just cutting and pasting off StackOverflow. Much of the code in production today lack originality and creativity required to solve hard problems.

Where did Curry-Howard breakdown?

Lecturas compartidas el 17 de marzo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-17-de-marzo #ATP #CurryHoward #FunctionalProgramming #Haskell #ILP #ITP #LambdaCalculus #Lean4 #Logic #LogicProgramming #Math #Programming #Python

Reification, Curry-Howard correspondence, and didactical consequences. ~ Reinhard Oldenburg. https://opus.bibliothek.uni-augsburg.de/opus4/frontdoor/deliver/index/docId/111981/file/111981.pdf #CurryHoward #FunctionalProgramming #LambdaCalculus

When Howard met Curry. ~ Rob Rix (@rob_rix). https://antitypical.com/posts/2021-07-28-when-howard-met-curry/ #Haskell #FunctionalProgramming #CurryHoward

A survey into the Curry-Howard isomorphism & type systems. ~ Phillip Mates. https://www.ccs.neu.edu/home/mates/pubs/mates_ugrad_thesis.pdf #Logic #Haskell #FunctionalProgramming #CurryHoward

The Curry-Howard correspondence in Haskell. ~ Tim Newsham. https://web.archive.org/web/20080819185521/http://www.thenewsh.com/~newsham/formal/curryhoward/ #Logic #Haskell #FunctionalProgramming #CurryHoward

Curry-Howard tutorial in literate Haskell. ~ Keith Pinson. https://gist.github.com/Kazark/06acabbd25817ac9efc7fbe0493f23ff #Haskell #FunctionalProgramming #Logic #CurryHoward

Haskell and the Curry-Howard isomorphism (Part 1). ~ Ben Sherman. https://www.ben-sherman.net/aux/curry-howard.pdf #Haskell #FunctionalProgramming #Logic #CurryHoward

Haskell and logic. ~ Rachel Lambda Samuelsson. https://rachel.cafe/2022/12/15/haskell-and-logic.html #Haskell #FunctionalProgramming #Logic #CurryHoward

In #CS, academics make much of #CurryHoward correspondence, and for many good reasons, too.

In #IT, there is the #HurryCoward aphorism: they who hurry code to production cower on the go-live day.

In this week's #blog I talk about a paper I know very well, Davies and Pfenning's 'A Modal Analysis of Staged Computation' https://updatedscholar.blogspot.com/2023/02/discussing-modal-analysis-of-staged.html #ModalLogic #CurryHoward

The #ANU #Logic #SummerSchool is all done. A lovely experience, although I also always find the performance of teaching quite draining. The slides for my lectures on #CurryHoward are up on http://lss.cecs.anu.edu.au/lectures/2022/2022/#ranald , along with slides from some of the other lecturers.

Good start (I think) this morning to my lecture series on #CurryHoward #PropositionsAsTypes at the #ANU #Logic #SummerSchool . My slides will appear at http://lss.cecs.anu.edu.au/lectures/2022/2022/#ranald across the week. Looking forward to attending Rosalie Iemhoff's lectures from tomorrow as well!