Bibliography

Hofmann, M. & Streicher, T. (1994)

, A groupoid model refutes uniqueness of identity proofs, in `Ninth Annual Symposium on Logic in Computer Science (LICS) (Paris, France)', IEEE, Computer Society Press, pp. 208-212.
URL: ftp://ftp.dcs.ed.ac.uk/pub/mxh/lics94.ps

Jones, C. (1991),

Completing the rationals and metric spaces in LEGO, in G. Huet, G. D. Plotkin & C. Jones, eds, `Proceedings of the Second Workshop on Logical Frameworks (Edinburgh, Scotland)', pp. 209-222.
URL: http://www.dcs.ed.ac.uk/lfcsinfo/research/types_bra/proc/ proc91.ps.gz

Luo, Z. (1993),

`Program specification and data refinement in type theory', Mathematical Structures in Computer Science 3, 333-363.
URL: http://www.dur.ac.uk/~dcs0zl/MSCS93.dvi

Luo, Z. (1994),

Computation and Reasoning: A Type Theory for Computer Science, Oxford University Press.

McKinna, J. H. (1992),

Delivarables: A Categorical Approach to Program Development in Type Theory, PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh.
URL: ftp://ftp.dcs.ed.ac.uk/pub/jhm/thesis.ps.gz