6 citations · 7 across the 2 of their papers we have counts for
3 papers
cs.LO2015
Semi-simplicial Types in Logic-enriched Homotopy Type Theory
Fedor Part, Zhaohui Luo
The problem of defining Semi-Simplicial Types (SSTs) in Homotopy Type Theory (HoTT) has been recognized as important during the Year of Univalent Foundations at the Institute of Ad…
cs.LO2011★ 1 cited
Typed Operational Semantics for Dependent Record Types
Yangyue Feng, Zhaohui Luo
Typed operational semantics is a method developed by H. Goguen to prove meta-theoretic properties of type systems. This paper studies the metatheory of a type system with dependent…
cs.LO2009★ 6 cited
Classical Predicative Logic-Enriched Type Theories
Robin Adams, Zhaohui Luo
A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTTO and LTTO*, which we…