Print this page

CiE 2006

Home page

General Information

CiE Network and Series

Programme Committee

Contact Info

Sponsors

Grants

Registration

Location

Travel Information

Last Minute News

Excursion

Conference Photo

Further Photos

Scientific Programme

Tutorials

Invited Talks

Special Sessions

Contributed Talks

Schedule

Session Chairs

Publications

Pre- and Post-conference Publications

Call for Papers

Paper Submission

Call for Informal Talks

Informal Talk Submission

Information for Authors

Regular Talk:
NdE - Normalization during Extraction

Abstract

We present a methodology for improving the implementation of the NbE (Normalization by Evaluation) normalization algorithm in call-by-value functional programming languages like SCHEME. Such optimizations are meant to heavily
(at least from an empirical, observational viewpoint) decrease the run-time complexity of the NbE-normalization of long sequences of nested term applications (t_n .. (t_2 (t_1 t_0))..). A situation of this kind occurs for example in the case
of the extraction of a modulus of uniform continuity for a closed term t of Goedel's T of type (nat=>nat)=>(nat=>nat).
The aforementioned extraction is by means of an author's adaptation of Kohlenbach's Monotone Dialectica Interpretation
(for the more efficient synthesis of majorants in NbE-normal form) and proceeds from a proof of the hereditarily extensional equality of t to itself. This example was implemented in the MINLOG proof-system, hence a machine DEMOnstration will be available for the NdE optimization of the call-by-value NbE-normalization.

websites: Arnold Beckmann

2006-06-28