Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

root @ master

Name Size Revision Age Author Comment
.gitignore 138 Bytes 0707b72c about 2 years tlitak LaTeX extraction begins
BoundsLists.v 20.2 KB 0e225959 about 2 years tlitak restructured: the first commit with BoundsLists
BoundsSubformulas.v 11.5 KB 0e225959 about 2 years tlitak restructured: the first commit with BoundsLists
HilbertIPCsetup.v 30.6 KB 0e225959 about 2 years tlitak restructured: the first commit with BoundsLists
Ruitenburg1984Aux.v 16 KB 00388114 about 2 years tlitak cleaned up Aux file, added alternative proof of...
Ruitenburg1984KeyTheorem.v 48.3 KB 2b87cf12 about 2 years tlitak I have working and certified optimized_bound! J...
Ruitenburg1984Main.v 9.12 KB 00388114 about 2 years tlitak cleaned up Aux file, added alternative proof of...
coqdoc.css 5.86 KB c48dc578 about 2 years tlitak committed a working version, before experimenti...
coqdoc.sty 5.36 KB 0707b72c about 2 years tlitak LaTeX extraction begins
f_p_exform1_10_length_fp_haskell.txt 1.41 MB 1b37f6de about 2 years tlitak We have generated code, absurd output of Haskel...
f_p_exform1_10_output.txt 3.04 MB 1c4a39d9 about 2 years tlitak Got the right function computing length for th...
make.sh 796 Bytes 0e225959 about 2 years tlitak restructured: the first commit with BoundsLists
ruitenburg_modified.hs 8.98 KB 0707b72c about 2 years tlitak LaTeX extraction begins

Latest revisions

# Date Author Comment
00388114 10/14/2015 05:18 AM tlitak

cleaned up Aux file, added alternative proof of Lemma 1.7, fixed compilation problem

0e225959 10/13/2015 07:58 PM tlitak

restructured: the first commit with BoundsLists

6a8831be 10/13/2015 03:17 AM tlitak

some modifications in the setup file

0707b72c 10/12/2015 03:23 AM tlitak

LaTeX extraction begins

1b37f6de 10/09/2015 12:41 PM tlitak

We have generated code, absurd output of Haskell on the example function etc.

1c4a39d9 10/09/2015 03:06 AM tlitak

Got the right function computing length for the iterated bound substitution and started with program extraction

d2e35f4b 10/08/2015 11:26 PM tlitak

need to fix a little ...

f155a3ed 10/08/2015 05:14 PM tlitak

in the middle of implementing length/occurrence and final output function

2b87cf12 10/08/2015 05:30 AM tlitak

I have working and certified optimized_bound! Just how cool is that?

1c02965f 10/07/2015 05:04 PM tlitak

almost done with basic bound ...

View all revisions | View revisions

Also available in: Atom