Deprecated: Function split() is deprecated in /srv/www/htdocs-cs/cie06/db-code.php on line 73

Deprecated: Function split() is deprecated in /srv/www/htdocs-cs/cie06/db-code.php on line 80
CiE 2006 - Regular Talk: - NdE - Normalization during Extraction
Computability in Europe 2006
Logical Approaches to Computational Barriers

Print current page  Print this page

Regular Talk:
NdE - Normalization during Extraction

Speaker: Mircea-Dan Hernest
Slot: Tue, 14:50-15:10, Faraday C (col. 3)


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
Warning: date(): It is not safe to rely on the system's timezone settings. You are *required* to use the date.timezone setting or the date_default_timezone_set() function. In case you used any of those methods and you are still getting this warning, you most likely misspelled the timezone identifier. We selected the timezone 'UTC' for now, but please set date.timezone to select your timezone. in /srv/www/htdocs-cs/cie06/conf-code.php on line 135
2006-06-28 Valid HTML 4.01! Valid CSS! eXTReMe Tracker hit counters by