## User login## Navigation |
## Category Theory## Philip Wadler: Category Theory for the Working HackerNothing you don't already know, if you are inteo this sort of thing (and many if not most LtU-ers are), but a quick way to get the basic idea if you are not. Wadler has papers that explain Curry-Howard better, and the category theory content here is very basic -- but it's an easy listen that will give you the fundamental points if you still wonder what this category thing is all about. To make this a bit more fun for those already in the know: what is totally missing from the talk (understandable given time constraints) is why this should interest the "working hacker". So how about pointing out a few cool uses/ideas that discerning hackers will appreciate? Go for it! By Ehud Lamm at 2016-08-07 17:26 | Category Theory | Lambda Calculus | Semantics | 106 comments | other blogs | 23434 reads
## Cakes, Custard, and Category TheoryEugenia Cheng's new popular coscience book is out, in the U.K. under the title Cakes, Custard and Category Theory: Easy recipes for understanding complex maths, and in the U.S. under the title How to Bake Pi: An Edible Exploration of the Mathematics of Mathematics:
Cheng, one of the Catsters, gives a guided tour of mathematical thinking and research activities, and through the core philosophy underlying category theory. This is the kind of book you can give to your grandma and grandpa so they can boast to their friends what her grandchildren are doing (and bake you a nice dessert when you come and visit :) ). A pleasant weekend reading. By Ohad Kammar at 2015-07-17 16:47 | Category Theory | Critiques | Fun | General | Semantics | Theory | login or register to post comments | other blogs | 6634 reads
## Conservation laws for free!In this year's POPL, Bob Atkey made a splash by showing how to get from parametricity to conservation laws, via Noether's theorem:
By Ohad Kammar at 2014-10-28 07:52 | Category Theory | Fun | Functional | Lambda Calculus | Scientific Programming | Semantics | Theory | Type Theory | 5 comments | other blogs | 15148 reads
## Seemingly impossible programsIn case this one went under the radar, at POPL'12, Martín Escardó gave a tutorial on seemingly impossible functional programs:
A shorter version (coded in Haskell) appears in Andrej Bauer's blog. By Ohad Kammar at 2014-10-22 09:57 | Category Theory | Fun | Functional | Paradigms | Semantics | Theory | 36 comments | other blogs | 14798 reads
## Luca Cardelli FestschriftEarlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:
Hopefully the videos will be posted soon. By Ohad Kammar at 2014-09-12 10:10 | Category Theory | Lambda Calculus | Misc Books | Semantics | Theory | Type Theory | 4 comments | other blogs | 6518 reads
## Dependently-Typed Metaprogramming (in Agda)Conor McBride gave an 8-lecture summer course on Dependently typed metaprogramming (in Agda) at the Cambridge University Computer Laboratory:
The lecture notes, code, and video captures are available online. As with his previous course, the notes contain many(!) mind expanding exploratory exercises, some of which quite challenging. By Ohad Kammar at 2013-08-30 07:34 | Category Theory | Functional | Lambda Calculus | Meta-Programming | Paradigms | Semantics | Teaching & Learning | Theory | Type Theory | 5 comments | other blogs | 14164 reads
## Lightweight Monadic Programming in MLLightweight Monadic Programming in ML
This is an intriguing paper, with an implementation in about 2,000 lines of OCaml. I'm especially interested in its application to probabilistic computing, yielding a result related to Kiselyov and Shan's Hansei effort, but without requiring delimited continuations (not that there's anything wrong with delimited continuations). On a theoretical level, it's nice to see such a compelling example of what can be done once types are freed from the shackle of "describing how bits are laid out in memory" (another such compelling example, IMHO, is type-directed partial evaluation, but that's literally another story). By Paul Snively at 2011-07-28 18:11 | Category Theory | Functional | Implementation | Semantics | Type Theory | 35 comments | other blogs | 17571 reads
## Kleisli Arrows of Outrageous FortuneKleisli Arrows of Outrageous Fortune
I discovered this Googling around in an attempt to find some decent introductory material to Kleisli arrows. This isn't introductory, but it's a good resource. :-) The good introductory material I found was this. By Paul Snively at 2011-05-14 15:19 | Category Theory | Functional | Type Theory | 6 comments | other blogs | 12954 reads
## A Lambda Calculus for Real AnalysisA Lambda Calculus for Real Analysis
Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX. By Paul Snively at 2010-02-16 22:00 | Category Theory | Functional | Lambda Calculus | Logic/Declarative | Meta-Programming | Semantics | Type Theory | 9 comments | other blogs | 12431 reads
## Simplicial DatabasesSimplicial Databases, David I. Spivak.
This is what happens when you try to take the existence of ORDER BY and COUNT in SQL seriously. :-) If you're puzzled by how a geometric idea like simplexes could show up here, remember that the algebraic view of simplicial sets is as presheaves on the category of finite total orders and order-preserving maps. Every finite sequence gives rise to a total order on its set of positions, and tables have rows and columns as sequences! |
## Browse archives## Active forum topics |

## Recent comments

2 days 21 hours ago

3 days 2 hours ago

3 days 17 hours ago

4 days 9 hours ago

4 days 20 hours ago

5 days 12 hours ago

5 days 22 hours ago

6 days 5 hours ago

6 days 5 hours ago

6 days 9 hours ago