User loginNavigation 
TheoryPropositions as TypesPropositions as Types, Philip Wadler. Draft, March 2014.
Philip Wadler has written a very enjoyable (Like busses: you wait two thousand years for a definition of “effectively calculable”, and then three come along at once) paper about propositions as types that is accessible to PLTlettantes. By Manuel J. Simoni at 20140307 16:38  Fun  History  Theory  34 comments  other blogs  8807 reads
The marriage of bisimulations and Kripke logical relations
CK Hur, D Dreyer, G Neis, V Vafeiadis (POPL 2012). The marriage of bisimulations and Kripke logical relations.
There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in MLlike languagesthat is, languages that combine features like higherorder functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged are bisimulations and Kripke logical relations (KLRs). While both approaches are powerful, their complementary advantages have led us and other researchers to wonder whether there is an essential tradeoff between them. Furthermore, both approaches seem to suffer from fundamental limitations if one is interested in scaling them to interlanguage reasoning.I understand the paper as offering an extension to bisimulation that handles the notion of hidden transitions properly and so allows a generalisation of KLRs to any systems that can be treated using bisimulations. Applications to verified compilation are mentioned, and everything has been validated in Coq. Copatterns: the final approach to codata?Andreas Abel and Brigitte Pientka's WellFounded Recursion with Copatterns; a Unified Approach to Termination and Productivity is one of my highlights of the justfinished ICFP 2013, but it makes sense to focus on the first paper on this work, published at POPL back in January.
Codata has been often discussed here and elsewhere. See notably the discussion on Turner's Total Functional Programming (historical note: this 2004 beautification of the original 1995 paper which had much of the same ideas), and on the categorytheoryinspired Charity language. Given those precedents, it would be easy for the quick reader to "meh" on the novelty of putting "observation" first (elimination rather than introduction rules) when talking about codata; yet the above paper is the first concrete, usable presentation of an observation in a practical setting that feels right, and it solves longstanding problem that current dependentlytyped languages (Coq and Agda) have. Coinduction has an even more prominent role, due to its massive use to define program equivalence in concurrent process calculi; the relevant LtU discussion being about Davide Sangiorgi's On the origins of Bisimulation, Coinduction, and Fixed Points. The POPL'13 paper doesn't really tell us how coinduction should be seen with copatterns. It does not adress the question of termination, which is the topic of the more recent ICFP'13 paper, but I would say that the answer on that point feels less definitive. 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  11037 reads
Types for Flexible ObjectsTypes for Flexible Objects, by Pottayil Harisanker Menon, Zachary Palmer, Alexander Rozenshteyn, Scott Smith:
An interesting paper I stumbled across quite by accident, it purports quite an ambitious set of features: generalizing previous work on firstclass cases while supporting subtyping, mutation, and polymorphism all with full type inference, in an effort to match the flexibility of dynamically typed languages. It does so by introducing a host of new concepts that are almostbutnotquite generalizations of existing concepts, like "onions" which are kind of a typeindexed extensible record, and "scapes" which are sort of a generalization of pattern matching cases. Instead of approaching objects via a record calculus, they approach it using its dual as variant matching. Matching functions then have degenerate dependent types, which I first saw in the paper Type Inference for FirstClass Messages with MatchFunctions. Interesting aside, Scott Smith was a coauthor on this last paper too, but it isn't referenced in the "flexible objects" paper, despite the fact that "scapes" are "matchfunctions". Overall, quite a dense and ambitous paper, but the resulting TinyBang language looks very promising and quite expressive. Future work includes making the system more modular, as it currently requires whole program compilation, and adding firstclass labels, which in past work has led to interesting results as well. Most work exploiting row polymorphism is particularly interesting because it supports efficient compilation to indexpassing code for both records and variants. It's not clear if onions and scapes are also amenable to this sort of translation. Edit: a previous paper was published in 2012, A Practical, Typed Variant Object Model  Or, How to Stand On Your Head and Enjoy the View. BigBang is their language that provides syntactic sugar on top of TinyBang. Edit 2: commas fixed, thanks! By naasking at 20130904 16:57  MetaProgramming  ObjectFunctional  Theory  Type Theory  42 comments  other blogs  14139 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  9828 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  20489 reads
Heap space analysis for garbage collected languagesHeap space analysis for garbage collected languages, by Elvira Albert, Samir Genaim, Miguel GómezZamalloa:
Similar work has been covered here in the past. By naasking at 20130629 15:01  Implementation  Theory  login or register to post comments  other blogs  11218 reads
Dependent Types for JavaScriptDependent Types for JavaScript, by Ravi Chugh, David Herman, Ranjit Jhala:
Some good progress on inferring types for a very dynamic language. Explicit type declarations are placed in comments that start with "/*:". /*: x∶Top → {ν ∣ite Num(x) Num(ν) Bool(ν)} */ function negate(x) { if (typeof x == "number") { return 0  x; } else { return !x; } } By naasking at 20130323 15:08  ObjectFunctional  Theory  Type Theory  128 comments  other blogs  18537 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  11585 reads

Browse archivesActive forum topics 
Recent comments
3 hours 49 min ago
7 hours 5 min ago
8 hours 21 min ago
13 hours 2 min ago
13 hours 52 min ago
14 hours 32 min ago
15 hours 37 min ago
16 hours 39 min ago
16 hours 44 min ago
17 hours 39 min ago