Author: David Wahlstedt
Title: Type Theory with First-Order Data Types and Size-Change Termination
Keywords: Type Theory, Dependent types, Lambda-calculus, Normalization, Size-Change Termination, Type system, Logical Framework, Reducibility, Pattern-matching, Term rewriting.
Abstract: 
We prove normalization for a dependently typed lambda-calculus
extended with first-order data types and computation schemata for
first-order size-change terminating recursive functions.
Size-change termination, introduced by C.S. Lee, N.D. Jones and A.M.
Ben-Amram, can be seen as a generalized form of structural
induction, which allows inductive computations and proofs to be
defined in a straight-forward manner.  The language can be used as a
proof system---an extension of Martin-L\"{o}f's Logical Framework.