Algorithmic aspects of type-based program synthesis

dc.contributor.advisorRehof, Jakob
dc.contributor.authorDudenhefner, Andrej
dc.contributor.refereeUrzyczyn, Pawel
dc.date.accepted2019-06-24
dc.date.accessioned2019-07-10T09:22:15Z
dc.date.available2019-07-10T09:22:15Z
dc.date.issued2019
dc.description.abstractIn 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.de
dc.identifier.urihttp://hdl.handle.net/2003/38127
dc.identifier.urihttp://dx.doi.org/10.17877/DE290R-20108
dc.language.isoende
dc.subjectType theoryen
dc.subjectInhabitationen
dc.subjectProgram synthesisen
dc.subjectComplexityen
dc.subject.ddc004
dc.subject.rswkTypentheoriede
dc.subject.rswkProgrammsynthesede
dc.subject.rswkKomplexitätde
dc.titleAlgorithmic aspects of type-based program synthesisde
dc.typeTextde
dc.type.publicationtypedoctoralThesisde
dcterms.accessRightsopen access
eldorado.secondarypublicationfalsede

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Dudenhefner_Andrej_thesis.pdf
Size:
1.73 MB
Format:
Adobe Portable Document Format
Description:
DNB
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
4.85 KB
Format:
Item-specific license agreed upon to submission
Description: