### Skapa referens, olika format (klipp och klistra)

**Harvard**

Wahlstedt, D. (2007) *Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion*. Göteborg : Chalmers University of Technology (Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, nr: 2660).

** BibTeX **

@book{

Wahlstedt2007,

author={Wahlstedt, David},

title={Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion},

isbn={978-91-7291-979-2},

abstract={<p>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. Our result holds under the assumption that the call relation of the recursive definitions is well-founded.</p>
<p>Recursive definitions can be read as intuitive specifications, which makes it easier to understand their intended meaning, compared to definitions that use only pre-defined recursion operators, called elimination rules in type theory. Pattern-matching definitions can be seen as the underlying mechanism with which we describe elimination rules. The arguments used to justify recursively defined elimination rules are essentially the same as those justifying pattern-matching definitions. The use of pattern-matching takes the proof system closer to the look and feel of a programming language like Haskell or ML.</p>
<p>We use the "Size-Change Principle for Program Termination" (C.S. Lee, N.D. Jones, A. Ben-Amram 2001) to establish that the recursive definitions have a well-founded call relation. The size-change criterion subsumes many known characterizations of terminating recursions, including primitive recursion and lexicographical ordering, but it also deals transparently with permuted arguments and mutual recursion. When instantiating the size-change relation for this criterion to be constructor decomposition, it corresponds closely to what we could call well-founded structural recursion.</p>},

publisher={Institutionen för data- och informationsteknik, Datavetenskap (Chalmers), Chalmers tekniska högskola,},

place={Göteborg},

year={2007},

series={Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, no: 2660Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, no: 34D},

note={viii,120p},

}

** RefWorks **

RT Dissertation/Thesis

SR Electronic

ID 45188

A1 Wahlstedt, David

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

YR 2007

SN 978-91-7291-979-2

AB <p>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. Our result holds under the assumption that the call relation of the recursive definitions is well-founded.</p>
<p>Recursive definitions can be read as intuitive specifications, which makes it easier to understand their intended meaning, compared to definitions that use only pre-defined recursion operators, called elimination rules in type theory. Pattern-matching definitions can be seen as the underlying mechanism with which we describe elimination rules. The arguments used to justify recursively defined elimination rules are essentially the same as those justifying pattern-matching definitions. The use of pattern-matching takes the proof system closer to the look and feel of a programming language like Haskell or ML.</p>
<p>We use the "Size-Change Principle for Program Termination" (C.S. Lee, N.D. Jones, A. Ben-Amram 2001) to establish that the recursive definitions have a well-founded call relation. The size-change criterion subsumes many known characterizations of terminating recursions, including primitive recursion and lexicographical ordering, but it also deals transparently with permuted arguments and mutual recursion. When instantiating the size-change relation for this criterion to be constructor decomposition, it corresponds closely to what we could call well-founded structural recursion.</p>

PB Institutionen för data- och informationsteknik, Datavetenskap (Chalmers), Chalmers tekniska högskola,

T3 Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, no: 2660Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, no: 34D

LA eng

LK http://www.cse.chalmers.se/alumni/davidw/wdt_phd_printed_version.pdf

OL 30