User loginNavigation 
Category TheoryA Logic for Parametric PolymorphismA Logic for Parametric Polymorphism, Gordon Plotkin and MartÃn Abadi.
By neelk at 20070413 22:27  Category Theory  Lambda Calculus  Semantics  Theory  login or register to post comments  other blogs  6419 reads
A 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  8235 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  6136 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  6434 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  10418 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  8285 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  8988 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  48371 reads

Browse archivesActive forum topics 
Recent comments
1 day 3 hours ago
4 days 25 min ago
6 days 8 hours ago
6 days 11 hours ago
1 week 6 hours ago
1 week 13 hours ago
1 week 17 hours ago
1 week 17 hours ago
1 week 19 hours ago
1 week 1 day ago