Verification of second-order functional programs [Elektronische Ressource] / von Markus Axel Aderhold

248

pages

English

Documents

2009

Écrit par
Markus Axel Aderhold

Publié par
technischen_universitat_darmstadt

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

248

pages

English

Ebook

2009

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

technischen_universitat_darmstadt

Publié le

01 janvier 2009

Nombre de lectures

Langue

English

Poids de l'ouvrage

1 Mo

Veri cation of Second-OrderFunctional ProgramsVom Fachbereich Informatikder Technischen Universit at DarmstadtgenehmigteDissertationvon Diplom-Informatiker Markus Axel Aderholdaus Darmstadtzur Erlangung des akademischen Grades einesDoktor-Ingenieurs (Dr.-Ing.)Referenten der Arbeit: Prof. Dr. Christoph WaltherProf. Dr. Heiko MantelTag der Einreichung: 27.04.2009Tag der mundlic hen Prufung: 14.07.2009Darmstadt, 2009Hochschulkennzi er D17AbstractFunctional programming languages such as Haskell or ML allow the pro-grammer to implement and to use higher-order procedures. A higher-orderprocedure gets a function as argument and applies this function to somevalues. For instance, procedure map applies a function to all elements of alist and returns the list of the result values.Verifying that a higher-order program satis es a certain property is par-ticularly challenging, because it involves reasoning about indirect functioncalls; for instance, a call map(f;l) directly calls procedure map and indirectlycalls function f if list l is non-empty. Using a higher-order procedure g, aproceduref can be de ned by higher-order recursion; i. e., proceduref (di-rectly) calls g and passes itself as an argument to g, which leads to indirectrecursive calls. These indirect recursive calls make reasoning about higher-order programs dicult.

Voir