User loginNavigation 
FunctionalFunctional Geometry and the Traite ́ de LutherieFunctional Geometry and the Traite ́ de Lutherie by Harry Mairson, Brandeis University.
The SizeChange Termination Principle for Constructor Based LanguagesThe SizeChange Termination Principle for Constructor Based Languages, by Pierre Hyvernat:
Looks like a relatively straightforward and complete description of a termination checker based on a notion of 'sized types' limited to firstorder programs. LtU has covered this topic before, although this new paper doesn't seem to reference that particular Abel work. By naasking at 20130919 01:59  Functional  Theory  login or register to post comments  other blogs  11038 reads
DependentlyTyped Metaprogramming (in Agda)Conor McBride gave an 8lecture 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 20130830 07:34  Category Theory  Functional  Lambda Calculus  MetaProgramming  Paradigms  Semantics  Teaching & Learning  Theory  Type Theory  5 comments  other blogs  9831 reads
Extensible Effects  An Alternative to Monad TransformersExtensible Effects  An Alternative to Monad Transformers, by Oleg Kiselyov, Amr Sabry and Cameron Swords:
A followup to Oleg's delimited continuation adaptation of Cartwright and Felleisen's work on Extensible Denotational Language Specifications, which is a promising alternative means of composing effects to the standard monad transformers. This work embeds a userextensible effect EDSL in Haskell by encoding all effects into a single effect monad using a novel open union type and the continuation monad. The encoding is very similar to recent work on Algebraic Effects and Handlers, and closely resembles a typed clientserver interaction ala coroutines. This seems like a nice convergence of the topics covered in the algebraic effects thread and other recent work on effects, and it's more efficient than monad transformers to boot. By naasking at 20130729 14:53  Functional  Logic/Declarative  Theory  Type Theory  22 comments  other blogs  20491 reads
How OCaml type checker works  or what polymorphism and garbage collection have in commonHow OCaml type checker works  or what polymorphism and garbage collection have in common
As usual with Oleg, there's a lot going on here. Personally, I see parallels with "lambda with letrec" and "callbypushvalue," although making the connection with the latter takes some squinting through some of Levy's work other than his CBPV thesis. Study this to understand OCaml type inference and/or MLF, or for insights into region typing, or, as the title suggests, for suggestive analogies between polymorphism and garbage collection. By Paul Snively at 20130310 16:25  Functional  Implementation  Type Theory  1 comment  other blogs  12801 reads
Visi.ioVisi.io comes from David Pollak and aims at revolutionizing building tablet apps, but the main attraction now seems to be in exploring the way data flow and cloud computing can be integrated. The screencast is somewhat underwhelming but at least convinces me that there is a working prototype (I haven't looked further than the website as yet). The vision document has some nice ideas. Visi.io came up recently in the discussion of the future of spreadsheets. By Ehud Lamm at 20121027 09:36  Functional  Logic/Declarative  Parallel/Distributed  2 comments  other blogs  10713 reads
Milner Symposium 2012The Milner Symposium 2012 was held in Edinburgh this April in memory of the late Robin Milner.
The programme consisted of academic talks by colleagues and past students. The talks and slides are available online. I particularly liked the interleaving of the personal and human narrative underlying the scientific journey. A particularly good example is Joachim Parrow's talk on the origins of the pi calculus. Of particular interest to LtU members is the panel on the future of functional programming languages, consisting of Phil Wadler, Xavier Leroy, David MacQueen, Martin Odersky, Simon PeytonJones, and Don Syme. By Ohad Kammar at 20121016 17:31  Functional  General  History  Parallel/Distributed  Semantics  Theory  3 comments  other blogs  11586 reads
CUFP 2012 TutorialsIf you are in Denmark in September you should attend. If not, raise a glass to salute what is now abundantly clear: FPLs are conquering the ("real") world. Koka a function oriented language with effect inference
Koka extends the idea of using row polymorphism to encode an effect system and the relations between them. Daan Leijen is the primary researcher behind it and his research was featured previously on LtU, mainly on row polymorphism in the Morrow Language. So far there's no paper available on the language design, just the slides from a Lang.Next talk (which doesn't seem to have video available at Channel 9), but it's in the program for HOPE 2012. By Daniel Yokomizo at 20120816 05:40  Functional  Software Engineering  Type Theory  3 comments  other blogs  14130 reads
Mechanized λ<sub>JS</sub>Mechanized λ_{JS}
More work on mechanizing the actual, implemented semantics of a real language, rather than a toy. By Paul Snively at 20120627 15:28  Functional  Javascript  Lambda Calculus  Semantics  6 comments  other blogs  10141 reads

Browse archivesActive forum topics 
Recent comments
1 hour 58 min ago
2 hours 23 min ago
2 hours 26 min ago
6 hours 13 min ago
6 hours 51 min ago
11 hours 18 min ago
14 hours 34 min ago
15 hours 49 min ago
20 hours 30 min ago
21 hours 21 min ago