Authors: Dudenhefner, Andrej
Title: Algorithmic aspects of type-based program synthesis
Language (ISO): en
Abstract: In the area of type-based program synthesis, the decision problem of inhabitation (given a type environment Gamma and a type tau, is there a term M such that M can be assigned the type tau in Gamma?) corresponds to existence of a program (term M) that satisfies the given specification (type tau) under additional assumptions (type environment Gamma). Inhabitation in typed lambda-calculi can be seen as functional program synthesis from scratch. Complementarily, inhabitation in combinatory logic can be seen as domain-specific program synthesis. Further restrictions on inhabitant search, such as principality and relevance restrictions, yield inhabitants that are more closely tied to given specifications. Alternatively, dimension, rank, order, and arity restrictions provide means to control the complexity of inhabitant search. This work provides an overview over following results in type-based program synthesis: PSpace-completeness of principal inhabitation in the simply typed lambda-calculus, undecidability of inhabitation in lambda-calculus with intersection types, undecidability of inhabitation in lambda-calculus with intersection types in bounded dimension, undecidability of inhabitation in subintuitionistic combinatory logic, (o+2)-ExpTime-completeness of inhabitation in combinatory logic with intersection types with instantiation of bounded order o, and ExpTime-hardness of intersection type unification.
Subject Headings: Type theory
Program synthesis
Subject Headings (RSWK): Typentheorie
Issue Date: 2019
Appears in Collections:LS 14 Software Engineering

Files in This Item:
File Description SizeFormat 
Dudenhefner_Andrej_thesis.pdfDNB1.77 MBAdobe PDFView/Open

This item is protected by original copyright

Items in Eldorado are protected by copyright, with all rights reserved, unless otherwise indicated.