Variants of the basic calculus of constructions |
| |
| Authors: | M. W. Bunder Jonathan P. Seldin |
| |
| Affiliation: | a School of Mathematics and Applied Statistics, University of Wollongong, N.S.W. 2522, Australia;b Department of Mathematics and Computer Science, University of Lethbridge, 4401 University Drive, Lethbridge, Alberta, Canada, T1K 3M4 |
| |
| Abstract: | In this paper, a number of different versions of the basic calculus of constructions that have appeared in the literature are compared and the exact relationships between them are determined. The biggest differences between versions are those between the original version of Coquand and the version in early papers on the subject by Seldin. None of these results is very deep, but it seems useful to collect them in one place. |
| |
| Keywords: | Calculus of constructions Typed λ -calculus Pure typed systems |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
