Home

Zhaohui__Luo


An extended calculus of constructions

Coercive subtyping in type theory

Developing reuse technology in proof engineering

Program specification and data refinement in type theory