Abstract
We present a denotational semantics of a type system with dependent types, where types are interpreted as finitary projections. We prove then the correctness of a type-checking algorithm w.r.t. this semantics. In this way, we can justify some simple optimisation in this algorithm. We then sketch how to extend this semantics to allow a simple record mechanism with manifest fields. © 2002 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Coquand, T., & Takeyama, M. (2002). An implementation of type:Type. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2277 LNCS, pp. 53–62). Springer Verlag. https://doi.org/10.1007/3-540-45842-5_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
