Conor McBride & friends have been working on Frank (here's a recent draft paper: http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-march2014.pdf http:

Conor McBride & friends have been working on Frank (here's a recent draft paper: http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-march2014.pdf http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-...). Frank's basically based on an extension of the CBPV calculus. As far as I know, Conor's also working on extending the core Frank calculus to the dependently-typed case, though this might take a bit.