- Beta-Conversion, Efficiently

Condoluci, Andrea

INF/01 Informatica

Type-checking in dependent type theories relies on conversion, i.e. testing given lambda-terms for equality up to beta-evaluation and alpha-renaming. Computer tools based on the lambda-calculus currently implement conversion by means of algorithms whose complexity has not been identified, and in some cases even subject to an exponential time overhead with respect to the natural cost models (number of evaluation steps and size of input lambda-terms). This dissertation shows that in the pure lambda-calculus it is possible to obtain conversion algorithms with bilinear time complexity when evaluation is carried following evaluation strategies that generalize Call-by-Value to the stronger case required by conversion.

2020-04-02

Tesi di dottorato

NonPeerReviewed

application/pdf

urn:nbn:it:unibo-25866

Condoluci, Andrea (2020) Beta-Conversion, Efficiently, [Dissertation thesis], Alma Mater Studiorum Università di Bologna. Dottorato di ricerca in Computer science and engineering