GSF: Gradual System F

GSF is gradual language that supports for explicit polymorphism. GSF satisfies all the expected properties of a gradual parametric language such as type safety, the static gradual guarantee, and parametricity. Although the dynamic gradual guarantee is not satisfied we prove that it is incompatible with parametricity (see paper). Nevertheless we establish a weaker version of this property that allows us to disprove several claims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity. In this tutorial we present IGSF, a web executable model of GSF implemented in Scala and React.js. IGSF shows interactive typing and reduction derivations for arbitrary source programs.

The tutorial covers:

• How to install and run a web interpreter for GSF
• A basic presentation of the language syntax
• IGSF in action through examples found in the paper

We provide four ways to access to IGSF (although we strongly recommend the first one!):

1. Using the online implementation at https://pleiad.cl/gsf.
2. With the virtual machine, which can be downloaded here
3. Local execution of binaries, which can be downloaded here.
4. Compilation and execution of the source code, which can be downloaded here.

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 October 10, 2018), then follow the instructions for points 2 to 4.

We have set up a virtual machine with an Ubuntu installation and Java 1.8. The virtual machine image was created with Virtual Box 5.1.18.

1. Install Virtual Box 5.1.18 or higher.
2. Import the Virtual Machine Image
3. Start the Virtual Machine
4. Use the following credentials to log in: username: dev , password: qwe123
5. Open a terminal. (Make sure you are at home.)
6. Run

   ./obsec-web/bin/obsec-web

This should start a server on port 9000. To open the ObSec Pad go to http://localhost:9000/obsec/

To run the ObSec Pad locally, all you need is Java 1.8. Also check that you have Java 1.8 in the path.

The following instructions are Unix valid commands. If you have Windows installed in your machine, you need to perform the corresponding commands.

1. Unzip the file.

   unzip obsec-web.zip

2. Go to the “obsec-web ” folder:

   cd obsec-web

3. Add run permissions to the binary file:

   chmod +x bin/obsec-web

4. And then run:

   ./bin/obsec-web

   This should start a server in the port 9000. To open the ObSec Pad, go to http://localhost:9000/obsec/

5. In case the port 9000 is already taken, run:

   ./bin/obsec-web -Dhttp.port=<available-port-number>

To compile IGSF you need to have installed:

1. Scala (http://www.scala-lang.org/)
2. SBT (http://www.scala-sbt.org/)
3. Node v8.9.1 (https://nodejs.org/)
4. JDK >= v1.8 (https://www.oracle.com/technetwork/java/javase/downloads/)

First we have to unzip the sources

unzip gsf-sources.zip  

Then we enter to application folder and we start the web server

cd gsf
cd sbt

For default, the application server is a SPA (single page application), where the frontend is loaded from a javascript file located in public/javascript/app.js. To compile this javascript file, you have to enter the node folder first. From the application folder:

cd node

Then we have to install node packages:

npm i

Then once all the packages have been installed, we proceed to build and copy the generated javascript file into the web server. To do this there is a convenient file called make:

./make

If the file does not have permission to run then run:

chmod +x make

The following screenshot shows how the ObSec Pad looks like

Note that even though we provide some predefined examples, we suggest you finish this tutorial first. It will help you understand the syntax of ObSec and how to define and use type-based declassification policies.

The ObSec Pad has the minimal functionality you expect for an interpreter:

• Details of the language syntax.
• Type checking. It gives you the type of the program or an error if the program is not well-typed or if it has a syntax error.
• Execution. If the program was well-typed (as the result of clicking “TYPECHECK!”), the interface will show a button to execute the program.