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:15] – [The virtual machine] mtoro | research:software:gradual-unions [2017/05/02 10:30] – [A first example] mtoro | ||
---|---|---|---|
Line 40: | Line 40: | ||
service gradual-unions start | service gradual-unions start | ||
</ | </ | ||
- | - We provide the restart and stop commands as well. | + | |
+ | | ||
To change the port of the application, | To change the port of the application, | ||
Line 48: | 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 72: | 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 101: | 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 131: | 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. |