Preview
Unable to display preview. Download preview PDF.
References
R. Backhouse. On the meaning and construction of the rules in Martin-Löf s theory of types. In A. Avron et al, editor, Workshop on General Logic. LFCS Report Series, ECS-LFCS-88-52, Dept. of Computer Science, University of Edinburgh, 1988.
R. Burstall and J. McKinna. Deliverables: an approach to program development in the calculus of constructions. LFCS report ECS-LFCS-91-133, Dept of Computer Science, University of Edinburgh, 1991.
Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2/3), 1988.
Th. Coquand. Metamathematical investigations of a calculus of constructions. manuscript, 1989.
Th. Coquand. An algorithm for testing conversion in Type Theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.
Th. Coquand and Ch. Paulin-Mohring. Inductively denned types. Lecture Notes in Computer Science, 417, 1990.
M. Dummett. The philosophical basis of intuitionistic logic. In H. Rose and J. Shepherdson, editors, Proc. of the Logic Colloquium, 1973. North Holland, 1975. Reprinted in P. Benacerraf and H. Putnam (eds.), Philosophy of Mathematics: selected readings, Campbridge University Press.
M. Dummett. The Logical Basis of Metaphysics. Duckworth, 1991.
P. Dybjer. An inversion principle for Martin-Löfs type theory. In P. Dybjer et al, editor, Workshop on Programming Logic. Programming Methodology Group, Report 54, 1989.
P. Dybjer. Inductive sets and families in Martin-Löfs type theory and their set-theoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.
H. Goguen and Z. Luo. Inductive data types: Well-ordering types revisited. submitted manuscript, 1991.
R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Proc. 2nd Ann. Symp. on Logic in Computer Science, 1987.
Z. Luo, R. Pollack, and P. Taylor. How to Use LEGO: a preliminary user's manual. LFCS Technical Notes LFCS-TN-27, Dept. of Computer Science, Edinburgh University, 1989.
Z. Luo. ECC, an extended calculus of constructions. In Proc. of the Fourth Ann. Symp. on Logic in Computer Science, Asilomar, California, U.S.A., June 1989.
Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Also as Report CST-65-90/ECS-LFCS-90-118, Department of Computer Science, University of Edinburgh.
Z. Luo. A problem of adequacy: conservativity of calculus of constructions over higher-order logic. Technical report, LFCS report series ECS-LFCS-90-121, Department of Computer Science, University of Edinburgh, 1990.
Z. Luo. A higher-order calculus and theory abstraction. Information and Computation, 90(1):107–137, 1991.
Z. Luo. Program specification and data refinement in type theory. Proc. of the Fourth Inter. Joint Conf. on the Theory and Practice of Software Development (TAPSOFT), 1991. Also as LFCS report ECS-LFCS-91-131, Dept. of Computer Science, Edinburgh University.
P. Martin-Löf. An intuitionistic theory of types: predicative part. In H.Rose and J.C.Shepherdson, editors, Logic Colloquium'73,1975.
P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löfs Type Theory: an introduction. Oxford University Press, 1990.
C.-E. Ore. The Extended Calculus of Constructions (ECC) with inductive types. To appear in Information and Computation, 1990.
R. Pollack. The theory of LEGO. manuscript, 1989.
R. Pollack. The Tarski fixpoint theorem. communication on TYPES e-mail network, 1990.
D. Prawitz. On the idea of a general proof theory. Synthese, 27, 1974.
J. Smith. The independence of Peano's fourth axiom from Martin-Löfs type theory without universes. Journal of Symbolic Logic, 53(3), 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Luo, Z. (1992). A unifying theory of dependent types: the schematic approach. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023883
Download citation
DOI: https://doi.org/10.1007/BFb0023883
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55707-4
Online ISBN: 978-3-540-47276-6
eBook Packages: Springer Book Archive