Sökning: "David Wahlstedt"

Hittade 2 avhandlingar innehållade orden David Wahlstedt.

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

    Författare :David Wahlstedt; Chalmers University of Technology; []

    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

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

    Författare :David Wahlstedt; Chalmers University of Technology; []
    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