Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Termination checking wit… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Termination checking with types

Artikel i vetenskaplig tidskrift
Författare Andreas Abel
Publicerad i RAIRO - Theoretical Informatics and Applications
Volym 38
Nummer/häfte 4
Sidor 277-319
ISSN 0988-3754
Publiceringsår 2004
Publicerad vid
Sidor 277-319
Språk en
Ämnesord type-based termination; sized types; inductive types; course-of-value recursion; bidirectional type checking; strong normalization
Ämneskategorier Data- och informationsvetenskap

Sammanfattning

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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?