The OLDER MinLog For Dialectica Page

[ last updated on 12 Nov 2007, created on 20 Mai 2006, latest is HERE ]

This page is the access point to the latest snap-shots of the Dialectica program-extraction modules for the proof-system MinLog. In fact, a full MinLog distribution is offered, which includes the latest and most up-to-date developpment of the Pure, the Light and the Monotone Dialectica extraction modules which are (for the moment) compatible (only) with the official MinLog distribution of 15 July 2005 . In Schedule: adaptation to the latest official MinLog. Hence a huge rewriting task, possibly the code will be more efficiently commented after this ... - The three Dialectica modules (pure, light and monotone) were merged into one file which now includes also the small separated bureaucratic code. The example files were changed accordingly to the new unified/polymorphic syntax. Now the procedure call is (DIA-extract KIND proof) where KIND is 'light 'pure or 'monot - the Dialectica modules and examples are now all contained into the directory "FI", all files nicely ordered and no garbage-files; this has been a huge clean-up operation, now only the useful files are there !!! - some improvements to the human-interface, but don't expect much! :) - added the Hereditarily Extensional Equality example for the triple sum
f,k |==> f(f(f(0))) + ... + f(f(f(k-1))) in "FI/heeq/SumExample.scm" - completed the comparative treatment of the 3 extractions from the Fibonnaci semi-classical proof in "FI/fib/" namely the original "fib.scm" for the BBS Refined A-translation, then "fib_PDI.scm" for the Pure Dialectica extraction and finally "fib_LFI.scm" for the Light Dialectica extraction

Installation Instructions

It is assumed that you have (Petite) Chez Scheme 7.0a installed on your Computer. A very useful option, particularly when working with the Petite Interpreter is to also have Emacs installed on your Computer.

The snapshots are a ZIP archive of the "minlog" folder and its contents. Simply replace "C:/minlog" in the file "minlog/init.scm" with your actual desired "minlogpath". If you work under (any) version of WinDose and unzip in the root folder "C:\" then no change in the "minlog/init.scm" is needed.

NEW as of 12 Nov 2007: one single extraction module, named newfiets.scm. The Pure (fiets.scm), the Light (light_fiets.scm) and the Monotone (mon_fiets.scm) Dialectica extraction modules (this for older snapshots), together with all the examples and test-cases which we implemented are stored in the "minlog/FI/" folder, where "FI" is an achronym for "Functional Interpretation" , i.e., the other name under which Goedel's Dialectica interpretation is known. Enjoy!

Contact and Technical Support

Should you have any questions about Installation or about Dialectica interpretations, it is O.K. to
write me at danher AT lix DOT polytechnique DOT fr
I promise to do my best to answer as soon as possible ...