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

Markus Axel Aderhold

Description

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.

Sujets

• Informatik

Informations

• Publié par: technischen_universitat_darmstadt
• Publié le: 01 janvier 2009
• Nombre de lectures: 22
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait