- Beta-Conversion, Efficiently
- Condoluci, Andrea <1990>
Subject
- INF/01 Informatica
Description
- 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.
Date
- 2020-04-02
Type
- Doctoral Thesis
- PeerReviewed
Format
- application/pdf
Identifier
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