Omari said:Do you have any references on this? I would like to understand better how this is used.Sources for program correctness and the relationship between CT and Computation:
Correctness (Ocaml Programming) (This lecture series taught me most of what I know about functional programming and also introduced me to Proving Correctness, the link is specifically about the latter).
Curry-Howard Correspondence (OCaml Programming) (From the same lecture series, explain Programs = Proofs)
The Curry-Howard Isomorphism for Dummies (A gentle overview of the correspondence)
Curry-Howard-Lambek Correspondence (Programs = Proofs = Categories Haskell wiki)
Types and Functions (From Category Theory for Programmers, this link specifically is a very gentle introduction to the relationship between type theory in programming and composability in CT)
Functional Completeness of Cartesian Categories (Lambeks paper about the correspondence)
Curry-Howard-lambek Correspondence (technical introduction)
Category Theory and Diagrammatic Reasoning (Technical)
Notions of Computation and Monads (Technical, pay attention to section titled A Categorical Semantics of Computation)
Physics, Topology, Logic, and Computation (Technical, goes in proof relationship between CT, Logic, and Computation and touches upon CT relationship with mathematics and physics)
From Design Patterns to Category Theory (Lecture series on designing software via CT)
Category Theory for Programmers (I already linked a section from this book, but in general its a design patterns book from a CT perspective)
I am not well versed in CT use in physics, I just know that it is used especially in those areas formalized in differential geometry and algebra. I assume its a tool in research programs for theoretical and mathematical physics. Again, a good place to start looking is results around the Category of Smooth Manifolds
"Notice that there's more than one way to combine numbers. You can add them together, but you can also multiply them. Could there be a common abstraction for that? What about objects that can somehow be combined, even if they aren't 'number-like'? The generalisation of such operations is a branch of mathematics called category theory, and it has turned out to be productive when applied to functional programming. Haskell is the most prominent example."
This sums it up nicely, thanks for posting. I mapped this from the link to the thread.
