Refining refinement types It was observed by Burstall that it is natural to consider programs paired with their proof of correctness. During program development, the proof can be constructed together with the program. Specifications there are taken to be types plus some predicate, in a context. This notion of "deliverable" was studied by McKinna in his thesis, where it was pointed out that in practice it is existence of a proof which matters, and moreover that it would be better to incorporate extensional equality into the theory since specifications only determine programs up to extensional equality. Pfenning introduced "refinement types" in order to add an extra level of expressiveness over the type theories of ML and LF. Rather than replace the existing theories with more expressive ones, he considered a class of refinement types, each of which is essentially a base type plus a predicate. We give a calculus which can be seen as extending the deliverables idea, by providing an account of refinement types as a type-theoretic formalisation of specifications, where our view of a specification is that it is given by some logical refinement of a type, and should be thought of as a per (in context) over the type, thus accounting for equality. We build a theory of refinement types on top of the simply-typed lambda calculus and allow dependency, in the form of dependent sums and products, at the level of refinement types. This allows more expressive specifications without a complicated underlying type theory. Equality on terms is stratified at refinement types, and a subtyping relation (or 'refinement') is given on the refinement types. We give a simple concrete semantics using `Henkin pers', and deduce consistency from soundness. We also prove a completeness result, though we see that the calculus does not match the per intuition entirely. For future work, we are currently combining the calculus with another system, of 'refinement terms', consisting of programs with indeterminates. This is intended to give a fully formalised refinement calculus based on this view of specifications.