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.2.18.

1. Install Virtual Box 5.2.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

   ./gsf/bin/gsf

This should start a server on port 9000. To open IGSF go to http://localhost:9000/gsf/

To run IGSF 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 gsf-bin.zip

2. Go to the “gsf ” folder:

   cd gsf-0.9

3. Add run permissions to the binary file:

   chmod +x bin/gsf

4. And then run:

   ./bin/gsf

   This should start a server in the port 9000. To open IGSF, go to http://localhost:9000/gsf/

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

   ./bin/gsf -Dhttp.port=<available-port-number>

To compile IGSF you need to have installed:

1. Scala (http://www.scala-lang.org/) (NOT REALLY?)
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/)

We start by unziping the sources.

unzip gsf-sources.zip  

Then we can proceed to compile the frontend, or skip this and go straight to compile the backend (frontend is pre-compiled in location public/javascript/app.js=

To compile this javascript file, you have to enter the node folder first.

1. From the application folder:

   cd node

2. Then we have to install node packages (it may take a while).

   npm i

3. Then once all the packages have been installed, we proceed to build and copy the generated javascript file into the web server. There is a convenient file that does this called make.

   ./make

   If the file does not have permission to run, then execute the following:

   chmod +x make

1. From the application folder we start SBT:

   sbt

2. Then we compile the application as follows (it may take a while the first time):

   compile

1. From the application folder we start SBT (unless you already started it):

   sbt

2. Then we start the web application as follows:

   run

1. From the application folder we start SBT (unless you already started it):

   sbt

2. Then to generate a zip file with all the binaries we execute:

   dist

SBT will generate the zip file located in target/universal/gsf-0.9.zip

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.