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

Termination checking with types

Andreas Abel (Institutionen för datavetenskap)
RAIRO - Theoretical Informatics and Applications (0988-3754). Vol. 38 (2004), 4, p. 277-319.
[Artikel, refereegranskad vetenskaplig]

The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces Lambda(mu)(+), a lambda-calculus with recursion, inductive types, subtyping and bounded quanti. cation. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

Nyckelord: type-based termination; sized types; inductive types; course-of-value recursion; bidirectional type checking; strong normalization

Denna post skapades 2013-06-17. Senast ändrad 2016-10-18.
CPL Pubid: 178629


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)


Data- och informationsvetenskap

Chalmers infrastruktur