Professor Zhaohui Luo

  1. 2018
  2. Published

    On Subtyping in Type Theories with Canonical Objects

    Lungu, G. & Luo, Z., Nov 2018, Types for Proofs and Programs: Post-proceedings of the 22nd Int. Conf. on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics, Vol. 97. p. 13:1-13:31 31 p. 13

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  3. Published

    Identity Criteria of Common Nouns and dot-types for Copredication

    Chatzikyriakidis, S. & Luo, Z., 2018, In : Oslo Studies in Language. 10, 2, p. 121-141 21 p.

    Research output: Contribution to journalArticle

  4. 2017
  5. Published

    Adjectival and Adverbial Modification: The View from Modern Type Theories

    Chatzikyriakidis, S. & Luo, Z., Mar 2017, In : Journal of Logic, Language and Information. 26, 1, p. 45–88 44 p.

    Research output: Contribution to journalArticle

  6. Published

    Dependent Event Types

    Luo, Z. & Soloviev, S., 2017, Logic, Language, Information, and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings. Springer, p. 216-228 13 p. (Lecture Notes in Computer Science; vol. 10388).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  7. 2016
  8. E-pub ahead of print

    Proof Assistants for Natural Language Semantics

    Chatzikyriakidis, S. & Luo, Z., 10 Nov 2016, Logical Aspects of Computational Linguistics. Celebrating 20 Years of LACL (1996–2016) : 9th International Conference, LACL 2016, Nancy, France, December 5-7, 2016, Proceedings. Springer Heidelberg, Vol. 10054. p. 85-98 14 p. (Lecture Notes in Computer Science; vol. 10054).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  9. Published

    A Linear Dependent Type Theory

    Luo, Z. & Zhang, Y., May 2016, TYPES 2016: Book of Abstracts. p. 69-70 2 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  10. Forthcoming

    Introduction: Modern Perspectives in Type Theoretical Semantics

    Chatzikyriakidis, S. & Luo, Z., 2016, (Accepted/In press) Modern Perspectives in Type Theoretical Semantics.

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  11. Forthcoming

    On the Interpretation of Common Nouns: Types v.s. Predicates

    Chatzikyriakidis, S. & Luo, Z., 2016, (Accepted/In press) Modern Perspectives in Type Theoretical Semantics. Springer

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  12. 2015
  13. E-pub ahead of print

    Using Signatures in Type Theory to Represent Situations

    Chatzikyriakidis, S. & Luo, Z., 25 Aug 2015, New Frontiers in Artificial Intelligence : JSAI-isAI 2014 Workshops, LENLS, JURISIN, and GABA, Kanagawa, Japan, October 27-28, 2014, Revised Selected Papers. Murata, T., Mineshima, K. & Bekki, D. (eds.). Springer, p. 172-183 12 p. (Lecture Notes in Computer Science; vol. 9067).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  14. Published

    A Lambek Calculus with Dependent Types

    Luo, Z., 2015, Types for Proofs and Programs.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  15. Published

    Individuation Criteria, Dot-types and Copredication: A View from Modern Type Theories

    Chatzikyriakidis, S. & Luo, Z., 2015, Proceedings of the 14th Meeting on the Mathematics of Language (MoL 2015). Association for Computational Linguistics, p. 39-50 12 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  16. In preparation

    Signatures in Formal Semantics (tentative title)

    Chatzikyriakidis, S. & Luo, Z., 2015, (In preparation) Modern Perspectives in Type-Theoretical Semantics. Chatzikyriakidis, S. & Luo, Z. (eds.). Springer, (Studies in Linguistics and Philosophy; vol. 98).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  17. 2014
  18. Published

    Natural Language Inference in Coq

    Chatzikyriakidis, S. & Luo, Z., Dec 2014, In : Journal of Logic, Language and Information. 23, 4

    Research output: Contribution to journalArticle

  19. Published

    Formal Semantics in Modern Type Theories: Is It Model-Theoretic, Proof-Theoretic, or Both?

    Luo, Z., 2014, Logical Aspects of Computational Linguistics: 8th International Conference, LACL 2014, Toulouse, France, June 18-24, 2014. Proceedings. Asher, N. & Soloviev, S. (eds.). Springer-Verlag, p. 177-188 12 p. (Lecture Notes in Computer Science; vol. 8535).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  20. Published

    Monotonicity Reasoning in Formal Semantics Based on Modern Type Theories

    Lungu, G. & Luo, Z., 2014, Logical Aspects of Computational Linguistics: 8th International Conference, LACL 2014, Toulouse, France, June 18-20, 2014. Proceedings. Asher, N. & Soloviev, S. (eds.). Springer, p. 138-148 11 p. (Lecture Notes in Computer Science; vol. 8535).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  21. Published

    Natural Language Reasoning Using Proof-assistant Technology: Rich Typing and Beyond

    Chatzikyriakidis, S. & Luo, Z., 2014, Proceedings of the EACL 2014 Workshop on Type Theory and Natural Language Semantics (TTNLS).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  22. Published

    Using Signatures in Type Theory to Represent Situations

    Chatzikyriakidis, S. & Luo, Z., 2014, JSAI International Symposium on Artificial Intelligence. p. 172-183 12 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  23. 2013
  24. Published

    Coercive subtyping: theory and implementation

    Luo, Z., Soloviev, S. & Xue, T., Feb 2013, In : Information and Computation. 223, p. 18-42

    Research output: Contribution to journalArticle

  25. Published

    A Pluralist Approach to Type-Theoretic Foundations.

    Luo, Z., 2013, Inter. Conf. on Type Theory, Homotopy Theory and Univalent Foundations. .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  26. Published

    Subtyping in Type Theory: Coercion Contexts and Local Coercions

    Luo, Z. & Part, F., 2013.

    Research output: Contribution to conferenceAbstract

  27. 2011
  28. Published

    A Pluralist Approach to the Formalisation of Mathematics

    Adams, R. & Luo, Z., 2 Jul 2011, In : Mathematical Structures in Computer Science. 21, 4, p. 913-942 29 p.

    Research output: Contribution to journalArticle

  29. Published

    Contextual analysis of word meanings in type-theoretical semantics

    Luo, Z., 2011, Logical Aspects of Computational Linguistics:6th International Conference, LACL 2011, Montpellier, France, June 29 – July 1, 2011: Proceedings. Pogodalla, S. & Prost, J-P. (eds.). Springer, p. 159-174 16 p. (Lecture Notes in Computer Science; vol. 6736).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  30. Published

    Typed Operational Semantics for Dependent Record Types

    Feng, Y. & Luo, Z., 2011, Proceedings of Types for Proofs and Programs (TYPES'09), EPTCS 53.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  31. 2010
  32. Published

    Classical Predicative Logic-Enriched Type Theories

    Adams, R. & Luo, Z., Aug 2010, In : Annals of Pure and Applied Logic. 161, 11, p. 1315-1345 31 p.

    Research output: Contribution to journalArticle

  33. Published

    Weyl's predicative classical mathematics as a logic-enriched type theory

    Adams, R. & Luo, Z., Jan 2010, In : ACM Transactions on Computational Logic. 11, 2, 31 p., 11.

    Research output: Contribution to journalArticle

  34. Published

    Type-Theoretical Semantics with Coercive Subtyping

    Luo, Z., 2010, Semantics and Linguistic Theory. Vol. 20. p. 38-56 19 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  35. 2009
  36. Published

    Dependent record types revisited

    Luo, Z., 2009, Modules and Libraries for Proof Assistants (MLPA'09), ACM Inter. Conf. Proceeding Series. Vol. 429.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  37. Published

    Manifest fields and module mechanisms in intensional type theory

    Luo, Z., 2009, Types for Proofs and Programs, Proc. of Inter. Conf. of TYPES'08. LNCS 5497. p. 237-255 18 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  38. 2008
  39. Published

    Coercions in a polymorphic type system

    Luo, Z., Aug 2008, In : Mathematical Structures in Computer Science. 18, 4, p. 729-751 23 p.

    Research output: Contribution to journalArticle

  40. Published

    Structural subtyping for inductive types with functorial equality rules

    Luo, Z. & Adams, R., 2008, In : Mathematical Structures in Computer Science. 18, 5, p. 931-972 42 p.

    Research output: Contribution to journalArticle

  41. 2007
  42. Published

    A type-theoretic framework for formal reasoning with different logical foundations

    Luo, Z., 2007, Advances in Computer Science, Proc of the 11th Annual Asian Computing Science Conference. LNCS 4435. Springer

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  43. Published

    Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory

    Adams, R. & Luo, Z., 2007, Types for Proofs and Programs. Altenkirch, T. & McBride, C. (eds.). Springer, Vol. 4502. p. 1-17 17 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  44. 2005
  45. Published

    LFTOP: an LF-based approach to domain-specific reasoning

    Pang, J., Callaghan, P. & Luo, Z., 2005, In : Journal of Computer Science and Technology. 20, 4, p. 526-535

    Research output: Contribution to journalArticle

  46. Published

    Transitivity in coercive subtyping

    Luo, Z. & Luo, Y., 2005, In : Infor. and Computation. 197, 1-2, p. 122-144 23 p.

    Research output: Contribution to journalArticle

  47. 2004
  48. Published

    Coercions in Hindley-Milner systems

    Kießling, R. & Luo, Z., 2004, Types for Proofs and Programs, Proc. of Inter. Conf. of TYPES'03. LNCS'3085.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  49. Published

    Combining incoherent coercions for Sigma-types

    Luo, Y. & Luo, Z., 2004, Types for Proofs and Programs, Proc. of Inter. Conf. of TYPES'03. LNCS'3085.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  50. 2003
  51. Published

    PAL+: a lambda-free logical framework

    Luo, Z., 2003, In : Journal of Functional Programming. 13, 2, p. 317-338 22 p.

    Research output: Contribution to journalArticle

  52. Published

    Weak Transitivity in Coercive Subtyping

    Luo, Y., Luo, Z. & Soloviev, S., 2003, Types for Proofs and Programs, Proc. of Inter Conf of TYPES'02. LNCS 2646. p. 220--239

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  53. 2002
  54. Published

    Coercion completion and conservativity in coercive subtyping

    Soloviev, S. & Luo, Z., 2002, In : Annals of Pure and Applied Logic. 113, 1-3, p. 297-322 26 p.

    Research output: Contribution to journalArticle

  55. Published

    Types for Proofs and Programs. Proc. of Inter. Conf. TYPES'2000, Durham, UK. LNCS 2277

    Callaghan, P. (ed.), Luo, Z. (ed.), McKinna, J. (ed.) & Pollack, R. (ed.), 2002, Springer.

    Research output: Book/ReportBook

  56. 2001
  57. Published

    An Implementation of LF with Coercive Subtyping and Universes.

    Callaghan, P. & Luo, Z., 2001, In : Journal of Automated Reasoning. 27, 1, p. 3-27 25 p.

    Research output: Contribution to journalArticle

  58. Published

    Coherence and transitivity in coercive subtyping

    Luo, Y. & Luo, Z., 2001, Proc. of the 8th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'01), LNAI 2250.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  59. Published

    Object languages in a type-theoretic meta-framework

    Callaghan, P. C., Luo, Z. & Pang, J., 2001, Proof Transformation and Presentation and Proof Complexities.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  60. 2000
  61. Published

    Implementation techniques for inductive types in Plastic

    Callaghan, P. & Luo, Z., 2000, Types for Proofs and Programs, Proc of Inter Conf of TYPES'99. LNCS 1956.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  62. Published

    PAL+: a lambda-free logical framework

    Luo, Z., 2000, Inter Workshop on Logical Frameworks and Meta-languages (LFM 2000).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  63. 1999
  64. Published

    Coercive subtyping

    Luo, Z., 1999, In : Journal of Logic and Computation. 9, 1, p. 105-130 26 p.

    Research output: Contribution to journalArticle

  65. Published

    Dependent coercions

    Luo, Z. & Soloviev, S., 1999, Proc of the 8th Inter. Conf. on Category Theory in Computer Science (CTCS'99), Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science, Vol 29.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  66. Published

    Lego and related work (summer school lecture notes)

    Luo, Z., 1999

    Research output: Other contribution

  67. Published

    Mathematical vernacular and conceptual well-formedness in mathematical language

    Luo, Z. & Callaghan, P., 1999, Proceedings of the 2nd Inter. Conf. on Logical Aspects of Computational Linguistics (LACL'97). LNAI 1582.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  68. 1998
  69. Published

    Coercive subtyping and lexical semantics (extended abstract)

    Luo, Z. & Callaghan, P., 1998, Logical Aspects of Computational Linguistics (LACL'98).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  70. Published

    Mathematical vernacular in type theory based proof assistants

    Callaghan, P. & Luo, Z., 1998, User Interfaces for Theorem Provers (UITP'98).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  71. Published

    Some proof-theoretic and algorithmic aspects of coercive subtyping

    Jones, A., Luo, Z. & Soloviev, S., 1998, Types for proofs and programs, Proc. of the Inter. Conf. TYPES'96, LNCS 1512.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  72. 1997
  73. Published

    A formal transformation and refinement method for re-engineering concurrent programs

    Younger, E., Bennett, K. & Luo, Z., 1997, Proc of IEEE Inter. Conf. on Software Maintenance.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  74. Published

    Coercive subtyping in type theory

    Luo, Z., 1997, CSL'96, LNCS'1258.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  75. Published

    Designing a Mathematical Vernacular (Invited talk at ESSLLI'97)

    Luo, Z. & Callaghan, P., 1997.

    Research output: Contribution to conferencePaper

  76. Published

    Implementing a model checker for Lego

    Yu, S. & Luo, Z., 1997, Proc. of the 4th Inter Symp. of Formal Methods Europe, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods. LNCS 1313.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  77. Published

    Linguistic categories in mathematical vernacular and their type-theoretic semantics (extended abstract)

    Luo, Z. & Callaghan, P., 1997, Logical Aspects of Computational Linguistics 97 (LACL'97).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  78. Published

    Proc of TYPES Working Group Workshop on Subtyping, Inheritance, and Modularisation of Proofs

    Luo, Z. (ed.) & Soloviev, S. (ed.), 1997, Durham University.

    Research output: Book/ReportBook

  79. 1996
  80. Published

    Logical truths in constructive type theory (abstract)

    Luo, Z., 1996, Logic Colloquium 96.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  81. Published

    Reverse engineering concurrent programs using formal modelling and analysis

    Younger, E., Luo, Z., Bennett, K. & Bull, T., 1996, Proc of IEEE Inter. Conf. on Software Maintenance.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  82. Published

    Type-theoretic semantics for SemNet

    Shiu, S., Luo, Z. & Garigliano, R., 1996, Proc. of Inter. Conf. on Formal and Applied Practical Reasoning, LNAI 1085.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  83. 1995
  84. Published

    Developing reuse technology in proof engineering

    Luo, Z., 1 Apr 1995, Proceedings of AISB95, Workshop on Automated Reasoning: bridging the gap between theory and practice, Sheffield, U.K..

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  85. Published

    Bylands: reverse engineering safety-critical systems

    Bull, T., Younger, E., Bennett, K. & Luo, Z., 1995, Proc. of Inter. Conf. on Software Maintenance.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  86. Published
  87. 1994
  88. Published

    Computation and Reasoning: A Type Theory for Computer Science

    Luo, Z., 1994, Oxford Univ Press. 228 p.

    Research output: Book/ReportBook

  89. 1993
  90. Published

    Inductive Data types: Well-Ordering Types Revisited

    Goguen, H. & Luo, Z., 1993, Logical Environments. Cambridge Univ Press

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  91. Published

    Program specification and data refinement in type theory

    Luo, Z., 1993, In : Mathematical Structures in Computer Science. 3, 3

    Research output: Contribution to journalArticle

  92. 1992
  93. Published

    A Set-theoretic Setting for Structuring Theories in Proof Development

    Luo, Z. & Burstall, R., 1992, LFCS Report Series. LFCS, Edinburgh Univ

    Research output: Chapter in Book/Report/Conference proceedingOther contribution

  94. Published

    A Unifying Theory of Dependent Types: the schematic approach

    Luo, Z., 1992, Proc. of Symp. on Logical Foundations of Computer Science (Logic at Tver'92), LNCS 620.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  95. Published

    LEGO Proof Development System: User's Manual

    Luo, Z. & Pollack, R., 1992, LFCS Report Series. LFCS, Edinburgh Univ

    Research output: Chapter in Book/Report/Conference proceedingOther contribution

  96. 1991
  97. Published

    A Higher-order Calculus and Theory Abstraction

    Luo, Z., 1991, In : Information and Computation. 90, 1, p. 107-137 31 p.

    Research output: Contribution to journalArticle

  98. Published

    Program specification and data refinement in type theory

    Luo, Z., 1991, Proc. of the Fourth Inter. Joint Conf. on the Theory and Practice of Software Development (TAPSOFT), LNCS 493.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  99. 1990
  100. Published

    A Problem of Adequacy: conservativity of calculus of constructions over higher-order logic

    Luo, Z., 1990, LFCS Report Series. LFCS, Edinburgh Univ

    Research output: Chapter in Book/Report/Conference proceedingOther contribution

  101. Unpublished

    An Extended Calculus of Constructions

    Luo, Z., 1990, (Unpublished) Univ of Edinburgh.

    Research output: ThesisDoctoral Thesis

  102. 1989
  103. Published

    ECC, an Extended Calculus of Constructions

    Luo, Z., 1 Jun 1989, Logics in Computer Science (LICS 1989).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  104. Published

    How to Use LEGO: a preliminary user's manual

    Luo, Z., Pollack, R. & Taylor, P., 1989, LFCS Technical Notes. LFCS, Edinburgh Univ

    Research output: Chapter in Book/Report/Conference proceedingOther contribution

  105. 1988
  106. Published

    A Higher-order Calculus and Theory Abstraction

    Luo, Z., 1988, LFCS Report Series.

    Research output: Chapter in Book/Report/Conference proceedingOther contribution

  107. Published

    CC# and Its Meta Theory

    Luo, Z., 1988, LFCS Report Series. LFCS, Edinburgh Univ

    Research output: Chapter in Book/Report/Conference proceedingOther contribution

  108. 1987
  109. Published

    The Foundations of Programming Methodology (程序方法学基础)

    Chen, H., Luo, Z. & Ma, Q., 1987, Hunan Press of Sciences.

    Research output: Book/ReportBook