Described are some experiments in the formalisation of the LISP programming language using LCF (Logic for Computable Functions.). The bulk of each experiment was concerned with applying the formalisation to proofs of correctness of some interesting LISP functions using Milner's mechanised version of LCF.nA definition of Pure LISP is given in an environment which includes an axiomatisation of LISP S-expressions. A primitive theory (a body of theorems in LCF) of Pure LISP is derived and is applied to proving the correctness of some simple LISP functions using the LCF proof checking system. A proof of correctness of McCarthy's interpreter is described and a machine checked proof of the partial correctness is outlined.nA more substantial subset of LISP and a subset of LAP (a LISP-oriented assembly language for the PDP-10 computer) were formalised and simple theories for the two languages were developed with computer assistance. This was done with a view to proving the correctness of a compiler, written the LISP subset, which translates LISP functions to LAP subroutines. The coarse structure of such a compiler correctness proof is displayed.
展开▼
