The following pages link to Zhaohui Luo (Q220709):
Displaying 41 items.
- Classical predicative logic-enriched type theories (Q636367) (← links)
- Adjectival and adverbial modification: the view from modern type theories (Q683682) (← links)
- Dependent event types (Q1685927) (← links)
- Transitivity in coercive subtyping (Q1776403) (← links)
- Coercive subtyping: theory and implementation (Q1951591) (← links)
- Natural language inference in Coq (Q2258817) (← links)
- A higher-order calculus and theory abstraction (Q2639838) (← links)
- (Q2736340) (← links)
- (Q2757819) (← links)
- (Q2766802) (← links)
- Weyl's predicative classical mathematics as a logic-enriched type theory (Q2946599) (← links)
- Proof Assistants for Natural Language Semantics (Q2963996) (← links)
- Coherence and Transitivity in Coercive Subtyping (Q2996166) (← links)
- Contextual Analysis of Word Meanings in Type-Theoretical Semantics (Q3010344) (← links)
- A pluralist approach to the formalisation of mathematics (Q3094181) (← links)
- (Q3211296) (← links)
- Coercions in a polymorphic type system (Q3520150) (← links)
- Structural subtyping for inductive types with functorial equality rules (Q3535679) (← links)
- Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory (Q3612432) (← links)
- Manifest Fields and Module Mechanisms in Intensional Type Theory (Q3638256) (← links)
- Coercive subtyping (Q4238487) (← links)
- (Q4246948) (← links)
- Mathematical vernacular and conceptual well-formedness in mathematical language (Q4263084) (← links)
- Program specification and data refinement in type theory (Q4282807) (← links)
- (Q4296744) (← links)
- (Q4362923) (← links)
- (Q4435472) (← links)
- <i>PAL</i><sup>+</sup>: a lambda-free logical framework (Q4457835) (← links)
- (Q4499226) (← links)
- (Q4599196) (← links)
- (Q4964710) (← links)
- Common Nouns as Types (Q4981255) (← links)
- Dot-types and Their Implementation (Q4981261) (← links)
- Monotonicity Reasoning in Formal Semantics Based on Modern Type Theories (Q4981275) (← links)
- Formal Semantics in Modern Type Theories: Is It Model-Theoretic, Proof-Theoretic, or Both? (Q4981278) (← links)
- Types for Proofs and Programs (Q5712310) (← links)
- Types for Proofs and Programs (Q5712311) (← links)
- An implementation of LF with coercive subtyping and universes (Q5951521) (← links)
- Coercion completion and conservativity in coercive subtyping (Q5957918) (← links)
- Propositional forms of judgemental interpretations (Q6053842) (← links)
- A metatheoretic analysis of subtype universes (Q6643039) (← links)
