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:18] – [The virtual machine] mtoro | research:software:gradual-unions [2017/05/02 10:44] – [Combining gradual unions and the unknown type] mtoro | ||
---|---|---|---|
Line 19: | Line 19: | ||
- **Using the online implementation** at [[https:// | - **Using the online implementation** at [[https:// | ||
- | - **With the provided virtual machine**, which can also be downloaded | + | - **With the provided virtual machine**, which can also be downloaded [[https:// |
- | - **Local execution of the prototype, which can be downloaded [[https:// | + | - **Local execution of the prototype**, which can be downloaded [[https:// |
The **online implementation** does not require any installation and is always up-to-date. If you want to get a snapshot of the current state of the interpreter (as of May 1, 2017), then follow the instructions for points 2 or 3. | The **online implementation** does not require any installation and is always up-to-date. If you want to get a snapshot of the current state of the interpreter (as of May 1, 2017), then follow the instructions for points 2 or 3. | ||
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. |
Each derivation tree can be expanded by clicking the button on the top-right corner: | Each derivation tree can be expanded by clicking the button on the top-right corner: | ||
Line 177: | Line 177: | ||
{{: | {{: | ||
- | This program, as we are passing a function from Int to Int the program run without errors. | + | This program |
Now consider the following program: | Now consider the following program: | ||