## User login## Navigation |
## Category Theory## 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 | 3670 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 | 11045 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 | 12370 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 | 10452 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 | 11000 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! ## An Innocent Model of Linear LogicAn Innocent Model of Linear Logic by Paul-André Melliès was referenced by Noam in a serendipitious subthread of the "Claiming Infinities" thread. Here's the abstract:
The introduction goes on to refer to to André Joyal's " Jacques Carette called this paper mind-blowing. My mind-blow warning light already exploded. I'm posting this paper because I know a number of LtUers are interested in these topics, and this way I can buttonhole one of them the next time I see them and ask them to explain it to me. ;) ## Lawvere Theories and MonadsMartin Hyland and John Power (2007). The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads. ENTCS 172:437-458. Both monads and Lawvere theories provide characterisations of algebraic structure, with monads providing the more general characterisation. The authors provide an introduction to Lawvere theories, discusses their relationship to sets, and why monads became the more popular treatment. Then they tackle the application of the theory to the semantics of side effects, where they argue that the generality of monads allow them to characterise computational phenomena that are not to do with side effects such as partiality and continuations, and argue that Lawvere theories more cleanly characterise what side effects are. This paper is a good introduction to an important line of recent research done by Hyland&Power; cf. also the LtU story Combining computational effects. ## Parameterized Notions of ComputationParameterized Notions of Computation, Robert Atkey, JFP 2008.
Once you've programmed with monads for a while, it's pretty common to start defining parameterized families of monads -- e.g., we might define a family of type constructors for IO, in which the program type additionally tracks which files the computation reads and writes from. This is a very convenient programming pattern, but the theory of it is honestly a little sketchy: on what basis do we conclude that the indices we define The application to delimited continuations is quite nice, and the type theories can also give a little insight into the basics of how stuff like Hoare Type Theory works (which uses parameterized monads, with a very sophisticated language of parameters). On a slightly tangential note, this also raises in my mind a methodological point. Over the last By neelk at 2009-02-11 21:40 | Category Theory | Lambda Calculus | Semantics | Type Theory | 16 comments | other blogs | 10386 reads
## Computation and the Periodic TableBy now there is an extensive network of interlocking analogies between physics, topology, logic and computer science, which can be seen most easily by comparing the roles that symmetric monoidal closed categories play in each subject. However, symmetric monoidal categories are just the n = 1, k = 3 entry of a hypothesized â€œperiodic tableâ€ of k-tuply monoidal n-categories. This raises the question of how these analogies extend. We present some thoughts on this question, focusing on how monoidal closed 2-categories might let us understand the lambda calculus more deeply. |
## Browse archives## Active forum topics |

## Recent comments

3 min 52 sec ago

3 hours 46 min ago

5 hours 41 min ago

9 hours 4 min ago

9 hours 4 min ago

9 hours 33 min ago

13 hours 34 min ago

13 hours 43 min ago

14 hours 48 min ago

15 hours 39 min ago