Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2009/10 / Oberseminar / Martin Hofmann: What is a pure functional?


Martin Hofmann: What is a pure functional?

29.01.2010 14:15
Wann 14:15 15:45 29.01.2010
von bis
Wo Z1.09 (neu: L109)
Termin übernehmen vCal
We investigate the following question. Given a higher-order SML function 
F : (int->int) -> int 
how can we rigorously specify that F is pure, ie produces no side-effects other than those arising from calling its functional argument. (If you don't like higher-order SML functions think of F as a method that may invoke a library function. It should produce no side-effects other than those that might arise from calls to the library function.) 
We show that existing methods based on preservation of invariants and relational parametricity are insufficient for this purpose and thus define a new notion that captures purity in the sense that for any functional F that is pure in this sense there exists a corresponding question-answer strategy, ie an element of the datatype 
type tree = Answer of int | Question of int * (int -> tree) 
This work is motivated by the ongoing effort to verify a new fixpoint algorithm by Helmut Seidl which takes such a functional as input (or rather a functional of type ((Variables->Domain)->(Variables->Domain)) and whose correctness is contingent on this functional to be pure.


abgelegt unter: