Normalising the associative law: An experiment with Martin-Löf's type theory (Q809071)

In the wide class of programming logics, which can be ``external'' or ``integrated'', constructive or classical, with partial or total objects, based on primitive or general recursion, etc., Martin-Löf's type theory has an integrated constructive logic, total objects, and general recursion. The purpose of the present paper is to show how Martin-Löf's type theory, despite of its initial characteristics mentioned, can also be successfully used: (1) as an external logic for verifying the correctness of an external program; (2) to integrate different proof techniques, such as measure functions, well-founded recursion, or the separation of correctness into termination and partial correctness, in order to obtain a correct type theory program; (3) to perform program derivations on the basis of C. Paulson's proof checker ISABELLE, splitting the programming problem into a computational part and a logical part; (4) to illustrate the use of inductively defined types and predicates in connection with Martin-Löf's type theory, viewed as an open system, for giving a more direct problem representation (e.g., an external program represented as a graph) than encodings using well- orderings. The concrete problem to which these ideas are applied is that of normalizing semigroup expressions with respect to the associative law.