- H. Maclean and Z. Luo. Subtype Universes. TYPES20. Turin, 2020. [pdf-file available]
- Z. Luo. Formal Semantics in Modern Type Theories: An Overview. Proof-Theoretic Semantics: Assessment and Future Perspectives, Proc. of the Third Tuebingen Conference on Proof-Theoretic Semantics. Tuebingen, 2019. [The abstract and slides are available.]
- Z. Luo. Substructural Calculi with Dependent Types. Linearity & TLLA (affiliaed with FLoC), Oxford. 2018. [This talk integrates the following two -- pdf-file available.]
- Z. Luo. A Lambek Calculus with Dependent Types. TYPES 2015. Tallinn, May 2015. [pdf-file available.]
- Z. Luo and Y. Zhang. A Linear Dependent Type Theory. TYPES 2016. Novi Sad, May 2016. [pdf-file available.]
- G. Lungu and Z. Luo. Definitional Extensions in Type Theorey Revisited. TYPES 2017. Budapest, May-June 2017.
- F. Part and Z. Luo. Semi-simplicial Types in Logic-enriched Homotopy Type Theory. 2015. [pdf-file available.]
- Z. Luo. A Pluralist Approach to Type-Theoretic Foundations. Inter. Conf. on Type Theory, Homotopy Theory and Univalent Foundations. Barcelona, Sept. 2013. (Also presented at Workshop on Foundation of Mathematics for Computer-Aided Formalization. Padova, Jan. 2013.)
- R. Adams and Z. Luo. Classical Predicative Logic-Enriched Type Theories. Annals of Pure and Applied Logic, 161(11). 2010. [pdf-file of the final version available.]
- R. Adams and Z. Luo. Weyl's predicative classical mathematics as a logic-enriched type theory. ACM Trans. on Computational Logic, 11(2). 2010. [pdf-file available.]
- Z. Luo. Dependent record types revisited. Proc. of the 1st Inter. Workshop on Modules and Libraries for Proof Assistants (MLPA'09), Montreal. ACM Inter. Conf. Proceeding Series; Vol. 429. 2009. [pdf-file of the final version available.]
- Y. Feng and Z. Luo. Typed Operational Semantics for Dependent Record Types. Proceedings of Types for Proofs and Programs (TYPES'09), Aussois, France. EPTCS 53, 2009. [pdf-file 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.]
- R. Adams and Z. Luo. Weyl's predicative classical mathematics as a logic-enriched type theory. In Types for Proofs and Programs, LNCS 4502. 2007. [pdf-file available.]
- Z. Luo. A type-theoretic framework for formal reasoning with different logical foundations. In Advances in Computer Science, Proc of the 11th Annual Asian Computing Science Conference. LNCS 4435. 2007. [pdf-file available.]
- Z. Luo. PAL+: a lambda-free logical framework. Journal of Functional Programming, 13(2), pp. 317-338. 2003. [ps file of the final version available.]
- Z. Luo. PAL+: a lambda-free logical framework. LFM'2000, Inter Workshop on Logical Frameworks and Meta-languages, Santa Barbara, California, 2000. [ps file available.]
- Z. Luo. Logical truths in constructive type theory (abstract). Logic Colloquium 96. 1996. [ps file available.]
- H. Goguen and Z. Luo. Inductive data types: well-ordering types revisited. In G. Huet and G. Plotkin (eds.), Logical Environments, Cambridge University Press, 1993. Also as ECS-LFCS-92-209, Dept of Computer Science, Edinburgh Univ. [pdf and ps files available.]
- Z. Luo. A unifying theory of dependent types: the schematic approach. Proc. of Symp. on Logical Foundations of Computer Science (Logic at Tver'92), LNCS 620, 1992. Also as ECS-LFCS-92-202, Dept of Computer Science, Edinburgh Univ. [ps file available.]
- Z. Luo. A problem of adequacy: conservativity of calculus of constructions over higher-order logic. ECS-LFCS-90-121, Dept of Computer Science, Edinburgh Univ, 1990. [pdf file available.]
- Z. Luo. A higher-order calculus and theory abstraction. Information and Computation 90(1), 1991. [ps file available.]
- Z. Luo. ECC: an Extended Calculus of Constructions. Proc. of IEEE 4th Ann. Symp. on Logic in Computer Science (LICS'89), Asilomar, California, 1989. [ps file available.]

Back to Zhaohui Luo's Publications page.