Type theory

• Z. Luo. Modern Type Theories: Their Development and Applications. Tsinghua University Press. 2024.


• 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).]


• 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 and pdf files of the final version available.]


• P. C. Callaghan, Z. Luo, J. H. McKinna and R. Pollack (eds.). Types for Proofs and Programs. Proc. of Inter. Conf. TYPES'2000, Durham, UK. LNCS 2277. 2002.


• 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 and pdf files available.]


• Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science, 11. Oxford University Press, 1994. (ISBN13: 978-0-19-853835-6; ISBN10: 0-19-853835-9)


• 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 and pdf files 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. [pdf and ps files available.]


• Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Also as Report CST-65-90/ECS-LFCS-90-118, Department of Computer Science, University of Edinburgh. [ pdf and ps files 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. [pdf and ps files available.]