Avancerad sökning

Hittade 2 avhandlingar som matchar ovanstående sökkriterier.

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

   Författare :David Wahlstedt; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES;

   Sammanfattning : 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. LÄS MER

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

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

   Sammanfattning : 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. LÄS MER