Next: About this document ...
Up: The LEGO library 
Previous: Natural Numbers: Basic theorems
 

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. 208212.
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. 209222.
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, 333363.
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