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:33] – [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 | + | Note as programs |
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. |