Defunctionalization at Work | Zendy

Olivier Danvy | Zendy; Lasse R. Nielsen | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Defunctionalization at Work

Author(s) -

Olivier Danvy,

Lasse R. Nielsen

Publication year - 2001

Publication title -

brics report series

Language(s) - English

Resource type - Journals

eISSN - 1601-5355

pISSN - 0909-0878

DOI - 10.7146/brics.v8i23.21684

Subject(s) - order (exchange) , bridge (graph theory) , correctness , computer science , mathematical proof , work (physics) , programming language , engineering , mathematics , mechanical engineering , business , medicine , geometry , finance

We study practical applications of Reynolds's defunctionalization technique, which is a whole-program transformation from higher-order to first-order functional programs. This study leads us to discover new connections between seemingly unrelated higher-order and first-order specifications and their correctness proofs. We thus perceive defunctionalization both as a springboard and as a bridge: as a springboard for discovering new connections between the first-order world and the higher-order world; and as a bridge for transferring existing results between first-order and higher-order settings.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research