## User login## Navigation |
## Theory## The Next Stage of StagingThe Next Stage of Staging, by Jun Inoue, Oleg Kiselyov, Yukiyoshi Kameyama:
A position paper describing the next logical progression of staging to metaprogramming over types. Now with the true first-class modules of 1ML, perhaps there's a clearer way forward. By naasking at 2015-03-29 13:34 | Functional | Meta-Programming | Theory | Type Theory | 57 comments | other blogs | 9368 reads
## Conservation laws for free!In this year's POPL, Bob Atkey made a splash by showing how to get from parametricity to conservation laws, via Noether's theorem:
By Ohad Kammar at 2014-10-28 07:52 | Category Theory | Fun | Functional | Lambda Calculus | Scientific Programming | Semantics | Theory | Type Theory | 5 comments | other blogs | 12370 reads
## Seemingly impossible programsIn case this one went under the radar, at POPL'12, Martín Escardó gave a tutorial on seemingly impossible functional programs:
A shorter version (coded in Haskell) appears in Andrej Bauer's blog. By Ohad Kammar at 2014-10-22 09:57 | Category Theory | Fun | Functional | Paradigms | Semantics | Theory | 36 comments | other blogs | 12175 reads
## sml-family.orgIn his blog, Bob Harper, in joint effort with Dave MacQueen and Lars Bergstrom, announces the launch of sml-family.org:
By Ohad Kammar at 2014-09-30 19:27 | Fun | Functional | History | Implementation | Paradigms | Semantics | Theory | 1 comment | other blogs | 7722 reads
## Inferring algebraic effectsLogical methods in computer science just published Matija Pretnar's latest take on algebraic effects and handlers:
Pretnar and Bauer's Eff has made previous appearances here on LtU. Apart from the new fangled polymorphic effect system, this paper also contains an Eff tutorial. By Ohad Kammar at 2014-09-27 23:16 | Functional | Implementation | Paradigms | Semantics | Theory | 8 comments | other blogs | 9526 reads
## Breaking the Complexity Barrier of Pure Functional Programs with Impure Data StructuresBreaking the Complexity Barrier of Pure Functional Programs with Impure Data Structures by Pieter Wuille and Tom Schrijvers:
This paper is along the same lines a question I asked a couple of years ago. The idea here is to allow programming using immutable interfaces, and then automatically transform it into a more efficient mutable equivalent. ## 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 | 5308 reads
## Propositions as TypesPropositions as Types, Philip Wadler. Draft, March 2014.
Philip Wadler has written a very enjoyable ( By Manuel J. Simoni at 2014-03-07 16:38 | Fun | History | Theory | 34 comments | other blogs | 13680 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 ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged areI 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 Well-Founded Recursion with Copatterns; a Unified Approach to Termination and Productivity is one of my highlights of the just-finished 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
category-theory-inspired 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 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. |
## Browse archives## Active forum topics |

## Recent comments

6 min 9 sec ago

43 min 8 sec ago

2 hours 25 min ago

2 hours 52 min ago

5 hours 22 min ago

5 hours 55 min ago

8 hours 21 min ago

11 hours 57 min ago

12 hours 3 min ago

12 hours 6 min ago