Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
research:software:gradual-unions [2017/05/02 10:16] – [The virtual machine] mtoro | research:software:gradual-unions [2017/05/02 10:30] – [A first example] mtoro | ||
---|---|---|---|
Line 49: | Line 49: | ||
/ | / | ||
</ | </ | ||
- | To run the application not as a service | + | To run the application not as a service, look at the next section (steps 4 and 5). |
Line 73: | Line 73: | ||
</ | </ | ||
- | To kill the application, | + | To kill the application, |
Note that to run again the implentation, | Note that to run again the implentation, | ||
Line 102: | Line 102: | ||
A term can be a typed lambda abstraction, | A term can be a typed lambda abstraction, | ||
- | Types can be booleans Bool, integers Int, unknown | + | Types can be booleans |
==== The action area ==== | ==== The action area ==== | ||
Line 132: | Line 132: | ||
{{: | {{: | ||
- | Each step shows in red the redux. | + | Each step shows the redux in red. |
- | Note as program may loop infinitely (we can encode omega), the prototype only present the first 10 steps of reduction. If after 10 steps of reduction the program is still reducible, another button is presented to reduce another 10 steps. | + | Note as program may loop infinitely (with ''?'' |
The reduction of the program is presented as the reduction of intrinsic terms: derivation trees augmented with evidence. An evidence reflects the justification of why a given consistent judgment holds. | The reduction of the program is presented as the reduction of intrinsic terms: derivation trees augmented with evidence. An evidence reflects the justification of why a given consistent judgment holds. |