Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Next revisionBoth sides next revision
research:software:gradual-unions [2017/05/02 10:15] – [The virtual machine] mtororesearch:software:gradual-unions [2017/05/02 10:34] – [A first example] mtoro
Line 40: Line 40:
 service gradual-unions start service gradual-unions start
 </code> </code>
-  - We provide the restart and stop commands as well.+  - If password is required, insert: 1234 
 +  - We also provide the restart and stop commands as well.
  
 To change the port of the application, just edit the file /etc/init.d/gradual-unions and change the value of the variable PORT. To change the port of the application, just edit the file /etc/init.d/gradual-unions and change the value of the variable PORT.
Line 48: Line 49:
 /home/gradualunions/gradual-unions-0.9/ /home/gradualunions/gradual-unions-0.9/
 </code> </code>
-To run the application not as a service just following steps 4 and 5.+To run the application not as a service, look at the next section (steps 4 and 5).
  
  
Line 72: Line 73:
 </code> </code>
  
-To kill the application, just press ctrl+c on the terminal running it, or kill the application with pid contained in file RUNNING_PID of the implementation folder.+To kill the application, just press ctrl+c on the terminal running it, or kill the application (the pid of the application is located in file RUNNING_PID of the implementation folder).
  
 Note that to run again the implentation, the RUNNING_PID file must be erased. Note that to run again the implentation, the RUNNING_PID file must be erased.
Line 101: Line 102:
  
 A term can be a typed lambda abstraction, a boolean, a number, a variable, an application, an addition, a conditional or an ascription. For convenience you can write an untyped lambda (\x.t) as a shortcut for (\x:?.t). A term can be a typed lambda abstraction, a boolean, a number, a variable, an application, an addition, a conditional or an ascription. For convenience you can write an untyped lambda (\x.t) as a shortcut for (\x:?.t).
-Types can be booleans Bool, integers Int, unknown types ? (which may represent any type), and gradual union types.+Types can be booleans (''Bool''), integers (''Int''), unknown type (''?'' -- which may represent any type), functions and gradual union types.
  
 ==== The action area ==== ==== The action area ====
Line 131: Line 132:
 {{:research:software:gradual-unions:typecheck.png?500|}} {{:research:software:gradual-unions:typecheck.png?500|}}
  
-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 programs may loop infinitely (with ''?'' we can encode omega), the prototype only presents 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.
  
-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: