Luo, Zhaohui Manifest fields and module mechanisms in intensional type theory. (English) Zbl 1246.68092 Berardi, Stefano (ed.) et al., Types for proofs and programs. International conference, TYPES 2008, Torino, Italy, March 26–29, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-02443-6/pbk). Lecture Notes in Computer Science 5497, 237-255 (2009). MSC: 68N19 03B15 PDFBibTeX XMLCite \textit{Z. Luo}, Lect. Notes Comput. Sci. 5497, 237--255 (2009; Zbl 1246.68092) Full Text: DOI
Luo, Zhaohui; Adams, Robin Structural subtyping for inductive types with functorial equality rules. (English) Zbl 1156.68017 Math. Struct. Comput. Sci. 18, No. 5, 931-972 (2008). MSC: 68N30 PDFBibTeX XMLCite \textit{Z. Luo} and \textit{R. Adams}, Math. Struct. Comput. Sci. 18, No. 5, 931--972 (2008; Zbl 1156.68017) Full Text: DOI
Luo, Zhaohui Coercions in a polymorphic type system. (English) Zbl 1153.68010 Math. Struct. Comput. Sci. 18, No. 4, 729-751 (2008). MSC: 68N18 PDFBibTeX XMLCite \textit{Z. Luo}, Math. Struct. Comput. Sci. 18, No. 4, 729--751 (2008; Zbl 1153.68010) Full Text: DOI