Search for dissertations about: "Size-Change Termination"

Found 2 swedish dissertations containing the words Size-Change Termination.

2. 1. Type Theory with First-Order Data Types and Size-Change Termination

   Author : David Wahlstedt; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; Pattern-matching; Reducibility; Size-Change Termination; Logical Framework; Lambda-calculus; Term rewriting.; Type Theory; Dependent types; Normalization; Type system;

   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. READ MORE

4. 2. Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion

   Author : David Wahlstedt; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES;

   Abstract : We present a variation of Martin-Löf's logical framework with "beta-iota-equality", extended with first-order parameterized algebraic data types and recursive pattern-matching definitions. Our contribution is a proof of normalization for the proposed system, from which we obtain decidable type-correctness. READ MORE