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 and pdf files 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 and pdf files 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. [pdf and ps file available.]


• Z. Luo. Developing reuse technology in proof engineering. Proc. of AISB95 Workshop on Automated Reasoning, Sheffield, UK, 1995. [pdf and ps files available.]


• 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 and pdf files 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 and pdf files available.]