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.


Previous | Index | Next