#### Proof development and proof assistants

- R. Adams and Z. Luo. A Pluralist Approach to the Formalisation of
Mathematics. Mathematical Structures in Computer Science, 21(4).
2011. [pdf file available]

- J. Pang, P.C. Callaghan and Z. Luo. LFTOP: an LF-based approach to
domain-specific reasoning. Journal of Computer Science and
Technology, 20(4), pp 526-535. 2005.

- P. C. Callaghan and Z. Luo. An implementation of LF with
coercive subtyping and universes. Journal of Automated Reasoning, 27(1),
pp 3-27. 2001.
[ps
file available.]

- P. C. Callaghan, Z. Luo and J. Pang. Object languages in a
type-theoretic meta-framework. Workshop of Proof Transformation and
Presentation and Proof Complexities,
Siena, Italy. 2001.
[ps
file available.]

- P. C. Callaghan and Z. Luo. Implementation techniques for inductive types in
Plastic.
In Types for Proofs and Programs, Proc of Inter Conf of TYPES'99. LNCS 1956. 2000.
[ps file available.]

- Z. Luo. Lego and related work. Lecture notes for the TYPES Summer School:
Theory and Practice of Formal Proofs, France, 1999. [ps
file available.]

- S. Yu and Z. Luo. Implementing a model checker for Lego. Proc. of the
4th Inter Symp. of Formal Methods Europe, FME'97: Industrial Applications
and Strengthened Foundations of Formal Methods, Graz, Austria. LNCS 1313,
1997. [ps file available.]

- Z. Luo. Developing reuse technology in proof engineering. Proc. of
AISB95 Workshop on Automated Reasoning, Sheffield, UK, 1995.

- Z. Luo and R. Burstall. A set-theoretic setting for structuring theories
in proof development. LFCS Report Series ECS-LFCS-92-206, Dept of Computer
Science, Edinburgh Univ, 1992. [ps
file available.]

- Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual.
ECS-LFCS-92-211, Dept of Computer Science, Edinburgh Univ, 1992. [ps file available.]

Back
to Zhaohui Luo's Publications page.