A Type Theory with Partially Defined Functions
 Publisher: UKC

Subject: QA76

References
(26)
[Alt93] Th. Altenkirch. Constructions, Inductive Types and Strong Normalization . PhD thesis, Edinburgh University, 1993.
[B+00] B. Barras et al. The Coq Proof Assistant Reference Manual (Version 6.3.1) . INRIARocquencourt, 2000.
[Bar84] H.P. Barendregt. The Lambda Calculus: its Syntax and Semantics. NorthHolland, revised edition, 1984.
[Bar92] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Clarendon Press, 1992.
[C+86] R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. PreticeHall, 1986.
[Coq92] Th. Coquand. Pattern matching with dependent types. Talk given at the BRA workshop on Proofs and Types, Bastad, 1992.
[Geu93] Herman Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.
[Gog94] H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.
[HHP87] R. Harper, F. Honsell, and G. Plotkin. A framework for dening logics. Proc. 2nd Ann. Symp. on Logic in Computer Science. IEEE, 1987.
[HHP92] R. Harper, F. Honsell, and G. Plotkin. A framework for dening logics. Journal of ACM, 40(1):143184, 1992.

Metrics
0views in OpenAIRE0views in local repository10downloads in local repository
The information is available from the following content providers:
From Number Of Views Number Of Downloads Kent Academic Repository  IRUSUK 0 10

 Download from


Cite this publication