next up previous contents
Next: About this document ... Up: The LEGO library - Previous: Natural Numbers: Basic theorems

References

-
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


Conor McBride
11/13/1998