## Using Constructions as a Metalanguage

**Paul Taylor**
*Abstract:* The Calculus of Constructions is a
lambda-calculus with dependent types, which provides a powerful
language for developing formal mathematics. In particular, by using
the same encoding ideas as the Edinburgh Logical Framework, it is
possible to express formal systems. Moreover the logic of
Constructions allows the development of inductive proofs and, as
the second-order lambda calculus is a subsystem, programs may be
defined and executed. This means that for a formal system expressed
within Constructions, there exists the possibility for proving and
applying admissible rules of the system. In this report we
illustrate this technique for the simple case of the equational
theory of semigroups: defining a canonical form theorem and a
decision procedure for the equality, for associative terms. The
proof within an interactive proof assistant for Constructions,
developed at Edinburgh by R. Pollack, is described.

*ECS-LFCS-89-70*

Previous |

Index |

Next