 | 2009 |
|---|
| 30 |       | Robin Adams,
Zhaohui Luo:
Classical Predicative Logic-Enriched Type Theories
CoRR abs/0906.1726: (2009) |
| 2008 |
|---|
| 29 | | Zhaohui Luo:
Manifest Fields and Module Mechanisms in Intensional Type Theory.
TYPES 2008: 237-255 |
| 28 | | Robin Adams,
Zhaohui Luo:
Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory
CoRR abs/0809.2061: (2008) |
| 27 | | Zhaohui Luo:
Coercions in a polymorphic type system.
Mathematical Structures in Computer Science 18(4): 729-751 (2008) |
| 26 | | Zhaohui Luo,
Robin Adams:
Structural subtyping for inductive types with functorial equality rules.
Mathematical Structures in Computer Science 18(5): 931-972 (2008) |
| 2006 |
|---|
| 25 | | Zhaohui Luo:
A Type-Theoretic Framework for Formal Reasoning with Different Logical Foundations.
ASIAN 2006: 214-222 |
| 24 | | Robin Adams,
Zhaohui Luo:
Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory.
TYPES 2006: 1-17 |
| 2005 |
|---|
| 23 | | Zhaohui Luo,
Yong Luo:
Transitivity in coercive subtyping.
Inf. Comput. 197(1-2): 122-144 (2005) |
| 22 | | Jian-Min Pang,
Paul Callaghan,
Zhaohui Luo:
LFTOP: An LF-Based Approach to Domain-Specific Reasoning.
J. Comput. Sci. Technol. 20(4): 526-535 (2005) |
| 2003 |
|---|
| 21 | | Robert Kießling,
Zhaohui Luo:
Coercions in Hindley-Milner Systems.
TYPES 2003: 259-275 |
| 20 | | Yong Luo,
Zhaohui Luo:
Combining Incoherent Coercions for Sigma-Types.
TYPES 2003: 276-292 |
| 19 | | Zhaohui Luo:
PAL+: a lambda-free logical framework.
J. Funct. Program. 13(2): 317-338 (2003) |
| 2002 |
|---|
| 18 |  | Paul Callaghan,
Zhaohui Luo,
James McKinna,
Robert Pollack:
Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers
Springer 2002 |
| 17 | | Yong Luo,
Zhaohui Luo,
Sergei Soloviev:
Weak Transitivity in Coercive Subtyping.
TYPES 2002: 220-239 |
| 2001 |
|---|
| 16 | | Yong Luo,
Zhaohui Luo:
Coherence and Transitivity in Coercive Subtyping.
LPAR 2001: 249-265 |
| 15 | | Zhaohui Luo:
Coercion completion and conservativity in coercive subtyping.
Ann. Pure Appl. Logic 113(1-3): 297-322 (2001) |
| 14 | | Paul Callaghan,
Zhaohui Luo:
An Implementation of LF with Coercive Subtyping & Universes.
J. Autom. Reasoning 27(1): 3-27 (2001) |
| 1999 |
|---|
| 13 | | Paul Callaghan,
Zhaohui Luo:
Implementation Techniques for Inductive Types in Plastic.
TYPES 1999: 94-113 |
| 12 | | Zhaohui Luo,
Sergei Soloviev:
Dependent Coercions.
Electr. Notes Theor. Comput. Sci. 29: (1999) |
| 11 | | Zhaohui Luo:
Coercive Subtyping.
J. Log. Comput. 9(1): 105-130 (1999) |
| 1997 |
|---|
| 10 | | Shenwei Yu,
Zhaohui Luo:
Implementing a Model Checker for LEGO.
FME 1997: 442-458 |
| 9 | | Zhaohui Luo,
Paul Callaghan:
Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language.
LACL 1997: 231-250 |
| 1996 |
|---|
| 8 | | Zhaohui Luo:
Coercive Subtyping in Type Theory.
CSL 1996: 276-296 |
| 7 | | Simon Shiu,
Zhaohui Luo,
Roberto Garigliano:
Type Theoretic Semantics for SemNet.
FAPR 1996: 582-595 |
| 6 | | Alex P. Jones,
Zhaohui Luo,
Sergei Soloviev:
Some Algorithmic and Proof-Theoretical Aspects of Coercive Subtyping.
TYPES 1996: 173-195 |
| 1993 |
|---|
| 5 | | Zhaohui Luo:
Program Specification and Data Refinement in Type Theory.
Mathematical Structures in Computer Science 3(3): 333-363 (1993) |
| 1992 |
|---|
| 4 | | Zhaohui Luo:
A Unifying Theory of Dependent Types: The Schematic Approach.
LFCS 1992: 293-304 |
| 1991 |
|---|
| 3 | | Zhaohui Luo:
Program Specification and Data Refinement in Type Theory.
TAPSOFT, Vol.1 1991: 143-168 |
| 2 | | Zhaohui Luo:
A Higher-Order Calculus and Theory Abstraction
Inf. Comput. 90(1): 107-137 (1991) |
| 1989 |
|---|
| 1 | | Zhaohui Luo:
ECC, an Extended Calculus of Constructions
LICS 1989: 386-395 |
