User loginNavigation 
Category TheoryA Topos Foundation for Theories of PhysicsA Topos Foundation for Theories of Physics: I. Formal Languages for Physics. Andreas Döring and Chris Isham.
This is a little outside of our usual areas, but I think it will appeal to at least some readers. Personally, I find the approach aesthetically very, very appealing for several reasons, and I would be thrilled if an answer to quantum cosmology came from this direction, but I'm the first to admit that my grasp of the phsyics is barely enough to follow along. I was able to make it through this paper fairly easily, but things aren't too interesting in the classical case, and I sadly suspect that the application to quantum physics in parts II and III will leave me behind. Via The nCategory Cafe, where there is also considerable discussion, much of it around the single word "peristalithic"... By Matt Hellige at 20070321 05:13  Category Theory  Type Theory  8 comments  other blogs  7976 reads
Propositions as [Types]Propositions as [Types], Steve Awodey and Adrej Bauer.
I figure I should say a few words about why proof irrelevance is an interesting idea. In math, you often want to consider elements of a certain type that have certain properties  for example, you might want the set of satisfiable boolean formulas as part of a proof as a hypothesis of a theorem. The way you might represent this in dependent type theory is by giving a pair, consisting of a formula and a satisfying assignment. You might write this as One way of addressing this problem is to treat the second component of the pair as a proof irrelevant type. The basic idea is that for each type I should also add that this is an old idea in type theory; this is the paper that made it clear to me. (Thanks to Bob Harper for suggesting clarifications to my comments.) By neelk at 20070303 19:19  Category Theory  Type Theory  5 comments  other blogs  5992 reads
Using Category Theory to Design Implicit Conversions and Generic OperatorsUsing Category Theory to Design Implicit Conversions and Generic Operators, John C. Reynolds, 1980. (Try this if the official link doesn't work.)
This is an old, but still cute, paper. The basic intuition is that a good design principle for a language with implicit conversions is that whatever order of conversions the language takes, you should get the same result. He then formalizes that by giving a category of types and conversions, and demanding that everything commute properly. And these give just the conditions the language designer has to check to make sure that he or she hasn't screwed anything up. Someone could probably get a fun little paper by taking this idea and shooting some dependent types into it. (Maybe somebody already has?) If you've got an abstract type, a coercion function, and a proof that it satisfies Reynolds' conditions, now your compiler can silently insert those coercions for you as needed, but you can still be sure that it won't mess up the meaning of your program. Holodeck games and CCCsFrom the nCategory Cafe, some notes on Holodeck Games and cartesian closed categories. This also appeared here (and was mentioned by Phil Wadler). The two posts seem to have different addenda, comments and links, so it may be worth looking at both. It's fun to see lambda calculus introduced to an audience already familiar with categories, as that seems to be the opposite of the usual state of affairs around here, and I can think of certain LtU regulars who will hopefully find this whole subject enjoyable. By Matt Hellige at 20061023 23:03  Category Theory  Fun  Lambda Calculus  login or register to post comments  other blogs  6341 reads
Arrows, like Monads, are MonoidsBy Chris Heunen and Bart Jacobs
By Jim Apple at 20060930 19:04  Category Theory  Functional  Lambda Calculus  3 comments  other blogs  10201 reads
Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach
By Jim Apple at 20060909 12:34  Category Theory  Functional  login or register to post comments  other blogs  8126 reads
Socially Responsive, Environmentally Friendly LogicSocially Responsive, Environmentally Friendly Logic
This paper seems to unify multiple interesting directions  logic, game semantics, concurrent constraint programming (and concurrent programming in general). At the same time it remains very accessible, without overwhelming amount of math, so can be hopefully useful not only for academics. I, for one, was waiting for exactly this kind of paper for two years (and my interest is very practical). Multiplayer CurryHoward correspondence, anyone? Or CurryHoward for web services? By Andris Birkmanis at 20060710 17:28  Category Theory  Logic/Declarative  Semantics  10 comments  other blogs  8712 reads
When is one thing equal to some other thing?For those of you still looking, here's a fun introduction to Category Theory by Barry Mazur. The Haskell Programmer's Guide to the IO Monad  Don't Panic
The Haskell Programmer's Guide to the IO Monad  Don't Panic. Stefan Klinger.
Why do I need a monad for IO in Haskell? The standard explanation is, that the IO monad hides the nonfunctional IO actions which do have side effects from the functional world of Haskell. But how does this "hiding" work, apart from having IO actions disappearing beyond the borders of my knowledge? It's hard for me to judge how successful this tutorial is going to be with beginners, but it seems well written. The target audience isn't porgrammers trying to learn about monads as a programming construct, but rather programmers that want to get a taste of theory. By Ehud Lamm at 20051215 20:47  Category Theory  Functional  22 comments  other blogs  45895 reads
Combining computational effectsWhile some researchers seek to generalize monads (to arrows), others try to narrow the focus to achieve a richer theory (and probably deeper understanding). Combining computational effects: commutativity and sum We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi's paradigm for modelling computational effects; we emphasise the importance here of the operations that induce computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi's sideeffects monad transformer (an application is the combination of sideeffects with nondeterminism). And we give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer (an application is the combination of exceptions with other effects).A longer version: Combining Effects: Sum and Tensor By Andris Birkmanis at 20051005 14:31  Category Theory  Semantics  3 comments  other blogs  11395 reads

Browse archivesActive forum topics 
Recent comments
2 weeks 2 days ago
2 weeks 2 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 5 days ago
2 weeks 6 days ago
3 weeks 4 days ago
3 weeks 5 days ago