CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

David Wahlstedt (Institutionen för datavetenskap, Programmeringslogik)
Göteborg : Chalmers University of Technology, 2004. - 60 s.

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öf's Logical Framework.

Nyckelord: Type Theory, Dependent types, Lambda-calculus, Normalization, Size-Change Termination, Type system, Logical Framework, Reducibility, Pattern-matching, Term rewriting.

Denna post skapades 2006-08-25. Senast ändrad 2013-07-05.
CPL Pubid: 16187


Institutioner (Chalmers)

Institutionen för datavetenskap, Programmeringslogik (2002-2004)



Chalmers infrastruktur


Datum: 2004-10-29

Ingår i serie

Technical report L - School of Computer Science and Engineering, Chalmers University of Technology 36