Coercive subtyping

• F. Bradley and Z. Luo. A Metatheoretic Analysis of Subtype Universes. Post-proceedings of the 28th Inter. Conf. on Types for Proofs and Programs (TYPES22). Leibniz International Proceedings in Informatics, Vol. 269. 2023. [The pdf-file is available and so are the pdf-file of an extended abstract, and the associated talk, for the TYPES23 conference in Valencia, Spain.]


• H. Maclean and Z. Luo. Subtype Universes. Post-proceedings of the 26th Inter. Conf. on Types for Proofs and Programs (TYPES20). Leibniz International Proceedings in Informatics, Vol. 188. 2021. [The pdf-file is available and so is the pdf-file of its extended abstract for the TYPES20 conference (planned in Torino, Italy, but did not take place because of the pandemic).]


• G. Lungu and Z. Luo. On Subtyping in Type Theories with Canonical Objects. Post-proceedings of the 22nd Int. Conf. on Types for Proofs and Programs (TYPES 2016), Leibniz International Proceedings in Informatics, Vol. 97. 2018. [pdf-file of the final version available.]


• Z. Luo, S. Soloviev and T. Xue. Coercive subtyping: theory and implementation. Information and Computation 223. 2013. [pdf-file available.]


• Z. Luo and F. Part. Subtyping in Type Theory: Coercion Contexts and Local Coercions. TYPES 2013, Toulouse, 2013. [Extended abstract available]


• Z. Luo. Manifest fields and module mechanisms in intensional type theory. In Types for Proofs and Programs, Proc. of Inter. Conf. of TYPES'08. LNCS 5497. 2009. [pdf-file available.]


• Z. Luo and R. Adams. Structural subtyping for inductive types with functorial equality rules. Mathematical Structures in Computer Science, 18(5), pp. 931-972. 2008. [pdf-file of the final version available.]


• Z. Luo. Coercions in a polymorphic type system. Mathematical Structures in Computer Science, 18(4), pp. 729-751. 2008. [pdf-file of the final version available.]


• Z. Luo and Y. Luo. Transitivity in coercive subtyping. Information and Computation, 197(1-2), pp 122-144. 2005. [ps and pdf files of the final version available.]


• R. Kiessling and Z. Luo. Coercions in Hindley-Milner systems. In Types for Proofs and Programs, Proc. of Inter. Conf. of TYPES'03. LNCS'3085. 2004. [ps and pdf files available.]


• Y. Luo and Z. Luo. Combining incoherent coercions for Sigma-types. In Types for Proofs and Programs, Proc. of Inter. Conf. of TYPES'03. LNCS'3085. 2004. [ps and pdf files available.]


• Y. Luo, Z. Luo and S. Soloviev. Weak transitivity in coercive subtyping. In Types for Proofs and Programs, Proc. of Inter Conf of TYPES'02. LNCS 2646. 2003. [pdf file available.]


• S. Soloviev and Z. Luo. Coercion completion and conservativity in coercive subtyping. Annals of Pure and Applied Logic. Vol 113(1-3), pp. 297-322. 2002. [ps and pdf files available.]


• Y. Luo and Z. Luo. Coherence and transitivity in coercive subtyping. Proc. of the 8th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'01), Havana, Cuba. LNAI 2250, 2001. [ps and pdf files available.]


• Z. Luo and S. Soloviev. Dependent coercions. Proc of the 8th Inter. Conf. on Category Theory in Computer Science (CTCS'99), Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science, Vol 29. 1999. [ps and pdf files available.]


• Z. Luo. Coercive subtyping. Journal of Logic and Computation. Vol. 9, No. 1. 1999 [ps and pdf files available.]


• A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. Types for proofs and programs, (eds.) E. Gimenez and C. Paulin-Mohring. LNCS 1512. 1998. [ps and pdf files available.]


• Z. Luo. Coercive subtyping in type theory. Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, 1997. [ps and pdf files available.]