Type theory and logical framework

• 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, 2011. [pdf-file available.]


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


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


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