Edit Profile (opens in new tab) Luo, Zhaohui Co-Author Distance Author ID: luo.zhaohui Published as: Luo, Zhaohui Homepage: https://www.cs.rhul.ac.uk/home/zhaohui/ External Links: GND Documents Indexed: 45 Publications since 1989, including 1 Book 1 Contribution as Editor · 1 Further Contribution Co-Authors: 13 Co-Authors with 28 Joint Publications 243 Co-Co-Authors all top 5 Co-Authors 14 single-authored 7 Solov’ëv, Sergeĭ Vladimirovich 5 Adams, Robin 5 Chatzikyriakidis, Stergios 4 Callaghan, Paul T. 4 Luo, Yong 2 Xue, Tao 1 Aczel, Peter 1 Ahrens, Benedikt 1 Altenkirch, Thorsten 1 Angiuli, Carlo 1 Avigad, Jeremy 1 Awodey, Steve 1 Barras, Bruno 1 Bauer, Andrej 1 Bertot, Yves 1 Bezem, Marc 1 Bordg, Anthony 1 Brunerie, Guillaume 1 Cohen, Cyril 1 Constable, Robert Lee 1 Coquand, Thierry 1 Curien, Pierre-Louis 1 Dybjer, Peter 1 Feng, Yangyue 1 Feng, Yuanyuan 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Harper, Robert 1 Herbelin, Hugo 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Hötzel Escardó, Martín 1 Hou (Favonia), Kuen-Bang 1 Jardine, John Frederick 1 Jones, Alex K. 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kießling, Robert 1 Kock, Joachim 1 Kraus, Nicolai 1 Li, Nuo 1 Licata, Dan 1 Lumsdaine, Peter LeFanu 1 Lungu, Georgiana E. 1 Mahboubi, Assia 1 Martin-Löf, Per 1 McKinna, James 1 Melikhov, Sergey Aleksandrovich 1 Nahas, Michael 1 Nie, Weifu 1 Palmgren, Erik 1 Pelayo, Alvaro 1 Pollack, Robert 1 Polonsky, Andrew 1 Riehl, Emily 1 Rijke, Egbert 1 Scott, Dana Stewart 1 Scott, Philip J. 1 Shulman, Michael A. 1 Sojakova, Kristina 1 Sozeau, Matthieu 1 Spitters, Bas 1 1 Van den Berg, Benno 1 Voevodskiĭ, Vladimir Aleksandrovich 1 Warren, Michael Alton 1 Xue, Taoxue 1 Zeilberger, Noam 1 Zhou, Yong all top 5 Serials 4 MSCS. Mathematical Structures in Computer Science 3 Information and Computation 3 Journal of Logic, Language and Information 2 Modern Physics Letters A 2 Annals of Pure and Applied Logic 1 Journal of Mathematical Physics 1 Mathematical Proceedings of the Cambridge Philosophical Society 1 Journal of Automated Reasoning 1 Journal of Logic and Computation 1 Journal of Functional Programming 1 ACM Transactions on Computational Logic 1 International Series of Monographs on Computer Science 1 Lecture Notes in Computer Science all top 5 Fields 33 Mathematical logic and foundations (03-XX) 30 Computer science (68-XX) 2 General and overarching topics; collections (00-XX) 2 Category theory; homological algebra (18-XX) 2 Quantum theory (81-XX) 2 Relativity and gravitational theory (83-XX) 1 Algebraic geometry (14-XX) 1 Partial differential equations (35-XX) 1 Algebraic topology (55-XX) 1 Fluid mechanics (76-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 35 Publications have been cited 162 times in 80 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 Computation and reasoning. A type theory for computer science. Zbl 0823.68101Luo, Zhaohui 32 1994 Coercive subtyping. Zbl 0920.03062Luo, Zhaohui 18 1999 ECC, an extended calculus of constructions. Zbl 0723.03034Luo, Zhaohui 17 1989 An implementation of LF with coercive subtyping and universes. Zbl 1023.03020Callaghan, Paul; Luo, Zhaohui 10 2001 Coercive subtyping: theory and implementation. Zbl 1267.03042Luo, Zhaohui; Soloviev, S.; Xue, Taoxue 9 2013 A higher-order calculus and theory abstraction. Zbl 0719.03004Luo, Zhaohui 8 1991 Contextual analysis of word meanings in type-theoretical semantics. Zbl 1333.03098Luo, Zhaohui 7 2011 Coercive subtyping in type theory. Zbl 0882.03029Luo, Zhaohui 6 1997 Natural language inference in Coq. Zbl 1305.68193Chatzikyriakidis, Stergios; Luo, Zhaohui 5 2014 Common nouns as types. Zbl 1291.03059Luo, Zhaohui 5 2012 Weyl’s predicative classical mathematics as a logic-enriched type theory. Zbl 1351.03002Adams, Robin; Luo, Zhaohui 4 2010 Transitivity in coercive subtyping. Zbl 1064.03021Luo, Zhaohui; Luo, Yong 4 2005 Formal semantics in modern type theories: is it model-theoretic, proof-theoretic, or both? Zbl 1291.03060Luo, Zhaohui 4 2014 Higher principal bundles. Zbl 1109.18007Jardine, J. F.; Luo, Z. 4 2006 Coercion completion and conservativity in coercive subtyping. Zbl 1011.03017Soloviev, Sergei; Luo, Zhaohui 4 2002 Proof assistants for natural language semantics. Zbl 1483.68456Chatzikyriakidis, Stergios; Luo, Zhaohui 3 2016 Adjectival and adverbial modification: the view from modern type theories. Zbl 1420.03055Chatzikyriakidis, Stergios; Luo, Zhaohui 3 2017 PAL\(^+\): A lambda-free logical framework. Zbl 1038.03035Luo, Zhaohui 3 2003 Weyl’s predicative classical mathematics as a logic-enriched type theory. Zbl 1178.03019Adams, Robin; Luo, Zhaohui 3 2007 Dot-types and their implementation. Zbl 1291.68406Xue, Tao; Luo, Zhaohui 2 2012 Coercions in a polymorphic type system. Zbl 1153.68010Luo, Zhaohui 2 2008 Some algorithmic and proof-theoretical aspects of coercive subtyping. Zbl 0927.03081Jones, Alex; Luo, Zhaohui; Soloviev, Sergei 2 1998 A unifying theory of dependent types: The schematic approach. Zbl 0978.03521Luo, Zhaohui 2 1992 Dependent event types. Zbl 1496.03056Luo, Zhaohui; Soloviev, Sergei 1 2017 Typed operational semantics for dependent record types. Zbl 1457.68154Feng, Yangyue; Luo, Zhaohui 1 2011 On the existence of local classical solutions to the Navier-Stokes equations with degenerate viscosities. Zbl 1422.76150Luo, Z.; Zhou, Y. 1 2019 Weak transitivity in coercive subtyping. Zbl 1023.68017Luo, Yong; Luo, Zhaohui; Soloviev, Sergei 1 2003 Monotonicity reasoning in formal semantics based on modern type theories. Zbl 1291.03058Lungu, Georgiana E.; Luo, Zhaohui 1 2014 Coherence and transitivity in coercive subtyping. Zbl 1275.03077Luo, Yong; Luo, Zhaohui 1 2001 Classical predicative logic-enriched type theories. Zbl 1231.03008Adams, Robin; Luo, Zhaohui 1 2010 Structural subtyping for inductive types with functorial equality rules. Zbl 1156.68017Luo, Zhaohui; Adams, Robin 1 2008 Dependent coercions. Zbl 0967.68047Luo, Zhaohui; Soloviev, Sergei 1 1999 Mathematical vernacular and conceptual well-formedness in mathematical language. Zbl 0934.03016Luo, Zhaohui; Callaghan, Paul 1 1999 Modified fermion tunneling radiation of Demianski-Newman black hole at higher energy scales. Zbl 1434.81137Luo, Z.; Lan, X. G. 1 2020 Modified fermion tunneling radiation of Demianski-Newman black hole at higher energy scales. Zbl 1434.81137Luo, Z.; Lan, X. G. 1 2020 On the existence of local classical solutions to the Navier-Stokes equations with degenerate viscosities. Zbl 1422.76150Luo, Z.; Zhou, Y. 1 2019 Adjectival and adverbial modification: the view from modern type theories. Zbl 1420.03055Chatzikyriakidis, Stergios; Luo, Zhaohui 3 2017 Dependent event types. Zbl 1496.03056Luo, Zhaohui; Soloviev, Sergei 1 2017 Proof assistants for natural language semantics. Zbl 1483.68456Chatzikyriakidis, Stergios; Luo, Zhaohui 3 2016 Natural language inference in Coq. Zbl 1305.68193Chatzikyriakidis, Stergios; Luo, Zhaohui 5 2014 Formal semantics in modern type theories: is it model-theoretic, proof-theoretic, or both? Zbl 1291.03060Luo, Zhaohui 4 2014 Monotonicity reasoning in formal semantics based on modern type theories. Zbl 1291.03058Lungu, Georgiana E.; Luo, Zhaohui 1 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 Coercive subtyping: theory and implementation. Zbl 1267.03042Luo, Zhaohui; Soloviev, S.; Xue, Taoxue 9 2013 Common nouns as types. Zbl 1291.03059Luo, Zhaohui 5 2012 Dot-types and their implementation. Zbl 1291.68406Xue, Tao; Luo, Zhaohui 2 2012 Contextual analysis of word meanings in type-theoretical semantics. Zbl 1333.03098Luo, Zhaohui 7 2011 Typed operational semantics for dependent record types. Zbl 1457.68154Feng, Yangyue; Luo, Zhaohui 1 2011 Weyl’s predicative classical mathematics as a logic-enriched type theory. Zbl 1351.03002Adams, Robin; Luo, Zhaohui 4 2010 Classical predicative logic-enriched type theories. Zbl 1231.03008Adams, Robin; Luo, Zhaohui 1 2010 Coercions in a polymorphic type system. Zbl 1153.68010Luo, Zhaohui 2 2008 Structural subtyping for inductive types with functorial equality rules. Zbl 1156.68017Luo, Zhaohui; Adams, Robin 1 2008 Weyl’s predicative classical mathematics as a logic-enriched type theory. Zbl 1178.03019Adams, Robin; Luo, Zhaohui 3 2007 Higher principal bundles. Zbl 1109.18007Jardine, J. F.; Luo, Z. 4 2006 Transitivity in coercive subtyping. Zbl 1064.03021Luo, Zhaohui; Luo, Yong 4 2005 PAL\(^+\): A lambda-free logical framework. Zbl 1038.03035Luo, Zhaohui 3 2003 Weak transitivity in coercive subtyping. Zbl 1023.68017Luo, Yong; Luo, Zhaohui; Soloviev, Sergei 1 2003 Coercion completion and conservativity in coercive subtyping. Zbl 1011.03017Soloviev, Sergei; Luo, Zhaohui 4 2002 An implementation of LF with coercive subtyping and universes. Zbl 1023.03020Callaghan, Paul; Luo, Zhaohui 10 2001 Coherence and transitivity in coercive subtyping. Zbl 1275.03077Luo, Yong; Luo, Zhaohui 1 2001 Coercive subtyping. Zbl 0920.03062Luo, Zhaohui 18 1999 Dependent coercions. Zbl 0967.68047Luo, Zhaohui; Soloviev, Sergei 1 1999 Mathematical vernacular and conceptual well-formedness in mathematical language. Zbl 0934.03016Luo, Zhaohui; Callaghan, Paul 1 1999 Some algorithmic and proof-theoretical aspects of coercive subtyping. Zbl 0927.03081Jones, Alex; Luo, Zhaohui; Soloviev, Sergei 2 1998 Coercive subtyping in type theory. Zbl 0882.03029Luo, Zhaohui 6 1997 Computation and reasoning. A type theory for computer science. Zbl 0823.68101Luo, Zhaohui 32 1994 A unifying theory of dependent types: The schematic approach. Zbl 0978.03521Luo, Zhaohui 2 1992 A higher-order calculus and theory abstraction. Zbl 0719.03004Luo, Zhaohui 8 1991 ECC, an extended calculus of constructions. Zbl 0723.03034Luo, Zhaohui 17 1989 all cited Publications top 5 cited Publications all top 5 Cited by 96 Authors 13 Luo, Zhaohui 6 Sacerdoti Coen, Claudio 5 Chatzikyriakidis, Stergios 5 Solov’ëv, Sergeĭ Vladimirovich 5 Tassi, Enrico 4 Geuvers, Jan Herman 4 Seldin, Jonathan P. 3 Adams, Robin 3 Asperti, Andrea 3 Avron, Arnon 3 Barthe, Gilles 3 Birkedal, Lars 3 Retoré, Christian 2 Aspinall, David 2 Compagnoni, Adriana B. 2 Fu, Yuxi 2 Harper, Robert 2 Møgelberg, Rasmus Ejlers 2 Pezlar, Ivo 2 Pollack, Robert 2 Ricciotti, Wilmer 1 Abel, Andreas M. 1 Akama, Yohji 1 Asher, Nicholas M. 1 Baranov, S. N. 1 Barendregt, Hendrik Pieter 1 Bauer, Andrej 1 Bernardy, Jean-Philippe 1 Bizjak, Aleš 1 Bos, Nathaniel 1 Bowen, Jonathan P. 1 Bunder, Martin W. 1 Castagna, Giuseppe 1 Chemouil, David 1 Chen, Gang 1 Clouston, Ranald A. 1 Constable, Robert Lee 1 Cooper, Robin 1 Cornes, Cristina 1 Crole, Roy L. 1 Dybjer, Peter 1 Fleuriot, Jacques D. 1 Forster, Yannick 1 Fridlender, Daniel 1 Garrigue, Jacques 1 Gillibert, Jean 1 Goguen, Healfdene 1 Grudzińska, Justyna 1 Guidi, Ferruccio 1 He, Jifeng 1 Honsell, Furio 1 Huang, Xuejing 1 Jojgov, Gueorgui I. 1 Kamareddine, Fairouz D. 1 Kozubek, Agnieszka 1 Lasson, Marc 1 Licata, Daniel R. 1 Luo, Yong 1 Malakhovski, J. 1 Mannaa, Bassel 1 Maskharashvili, Aleksandre 1 Mason, Ian A. 1 McBride, Conor Thomas 1 Monnier, Stefan 1 Moot, Richard 1 Morrisett, Greg 1 Nanevski, Aleksandar 1 Nederpelt, Rob 1 Obua, Steven 1 Oliveira, Bruno C.d. S. 1 Ore, Christian-Emil 1 Pagano, Miguel 1 Pitts, Andrew M. 1 Pollack, Randy 1 Raclavský, Jiří 1 Ranta, Aarne 1 Real, Livy 1 Ruys, Mark 1 Sato, Masahiro 1 Scott, Dana Stewart 1 Scott, Phil 1 Sheng, Feng 1 Simpson, Alex K. 1 Spitters, Bas 1 Terrasse, Delphine 1 Urzyczyn, Paweł 1 Voevodskiĭ, Vladimir Aleksandrovich 1 Wells, Joe B. 1 Wiedijk, Freek 1 Xue, Tao 1 Yang, Zongyuan 1 Zacchiroli, Stefano 1 Zawadowski, Marek W. 1 Zhao, Jinxu 1 Zhu, Huibiao 1 Zwanenburg, Jan all top 5 Cited in 18 Serials 10 MSCS. Mathematical Structures in Computer Science 8 Journal of Logic, Language and Information 5 Information and Computation 4 Theoretical Computer Science 4 Annals of Pure and Applied Logic 4 Journal of Applied Logic 3 Journal of Functional Programming 2 Journal of Computer Science and Technology 2 Journal of Automated Reasoning 2 Formal Aspects of Computing 2 Journal of Mathematical Sciences (New York) 2 RAIRO. Theoretical Informatics and Applications 1 Journal of Symbolic Computation 1 Indagationes Mathematicae. New Series 1 The Bulletin of Symbolic Logic 1 Logic and Logical Philosophy 1 Logica Universalis 1 Logical Methods in Computer Science all top 5 Cited in 9 Fields 58 Mathematical logic and foundations (03-XX) 52 Computer science (68-XX) 6 Category theory; homological algebra (18-XX) 2 History and biography (01-XX) 2 Algebraic topology (55-XX) 1 General and overarching topics; collections (00-XX) 1 Group theory and generalizations (20-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Biology and other natural sciences (92-XX) Citations by Year