-
Notifications
You must be signed in to change notification settings - Fork 5
/
notes.txt
83 lines (61 loc) · 2.3 KB
/
notes.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
08/27/2012
timing for divide and conquer add:
- 5 size 470 time 10s
- 6 size 942 time 62s
- 7 size 1886 time 408s
- 8 size 3774 time 2836s
With better bdds
- 5 size 470 time 10s
- 6 size 942 time 61s
- 7 size 1886 time 392s
With better bdds
- 5 size 470 time 10s
- 6 size 942 time 58s
- 7 size 1886 time 372s
06/01/2012 Discussion with Adam
- Mentionned the semantics issues with double-update errors treated as
guard errors. This has some impact on the number of multiplexers at
the end (and on the semantics of course, because more programs are
correct).
- Mentionned the fact that there shall be no bind errors (which were
real errors). This has impact on the semantics of register files,
which cannot be accessed out of bounds. Otherwise we have the tricky
situation that try (check false; x <- \bot) is different from x <-
\bot; try (check false).
- Discussion about the coq workshop proposal.
05/16/2012 Discussion with Adam
Discussion about the translation and about a potential paper. My
translation issues should be resolved by keeping PHOAS, and using a
proof similar to the one in ltamer/examples/untyped/CC.v
Paper
Section 1. Language.
- Core + Match + Sigma -> Core -> RTL
- Proofs of the previous
Section 2. Examples
- Mod, Isa, Pipelined (MIPS ?)
Section 3. Free stuff
- Scheduler
- Type system to prevent some bad stuff to happen
- Hoare/VCG
- Meta-level definition
- Compliance to a protocol / refinement
Section 4. Ripe Lava.
Question to ask to Arvind: to what kind of conference should we
submit this.
Shown the example of the coffe machines
05/10/2012 Discussion with Richard.
- GCD -> MOD.
- Turns out that to avoid having to use the scheduler, one may just
use "a orElse b" composition of actions, and "a ; b", and use wires to
implement sequential composition...
05/07/2012
Provided core GAA with a formal 'monadic' semantics, with a mixture of
PHOAS, and dependent de Bruijn indices.
05/02/2012
The user has to specify a schedule between the rules. A scheduler
cannot make a fair schedule between two rules that both apply. Or a
round robin ?
04/19/2012 Meeting
- Investigate the use of PHOAS for the definition of the embedding of TRS.
- Investigate the chapter of CPDT called Generic programming to
discover if Coq inductives could be used instead of the deep-embedding