Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system. Code accompanying the paper has been developed into an Agda library AoPA.
The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. This seems like it's related to Adam Chlipala's A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. See, in particular, slides 23-24 of this presentation (PDF). More generally, computation and reflection seem to be gaining recognition as important features for the practical use of Coq Again, the point is to simplify programming with dependent types in Coq
The abstract: We propose a novel, comonadic approach to dataflow (streambased) computation. This is based on the observation that both general and causal stream functions can be characterized as coKleisli arrows of comonads and on the intuition that comonads in general must be a good means to structure context-dependent computation. In particular, we develop a generic comonadic interpreter of languages for context-dependent computation and instantiate it for stream-based computation. We also discuss distributive laws of a comonad over a monad as a means to structure combinations of effectful and context-dependent computation. If you've ever wondered about dataflow or comonads, this paper is a good read. It begins with short reviews of monads, arrows, and comonads and includes an implementation. One feature that stood out is the idea of a higher-order dataflow language.
I had mistakenly learned that curry was a form of generalized partial application from the paper : Function Currying in Scheme by Jeffrey A. Meunier In my paper I defined curry in Cat as: define curry : ('b ('A 'b -> 'C) -> ('A -> 'C)) { swap quote swap compose } Whereas this really should have been called "partial-apply", "papply" or something comparable. So the correct definition should have been: define papply : ('b ('A 'b -> 'C) -> ('A -> 'C)) { swap quote swap compose } define curry : (('A 'b -> 'C) -> ('b -> ('A -> 'C)) { quote [papply] compose }