Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
..
Failed to load latest commit information.
doc
proof-ec
proof
.gitignore
Makefile
README.md

README.md

A Simple Soundness Proof for Dependent Object Types

Our paper presents a simplified type-safety proof for the version of DOT presented at Wadlerfest 2016. This repository contains a formalization of the simple proof in Coq. The definitions of the abstract syntax and several lemmas are based on the original Coq proof that comes with Wadlerfest DOT paper.

This directory contains a Coq formalization of the DOT calculus and DOT's type safety proof. Our technique is based on eliminating bad bounds by using inert types and applying the proof recipe, as described in the OOPSLA'17 paper.

Documentation

The documentation can be accessed from the table of contents. This page lists links to pretty printed Coq source files, but the raw .v files can be found in the proof directory. In the pretty-printed versions, the proof scripts are hidden by default, you may click on "Show Proofs" at the top of the page to display all the proofs, or click under the Lemma or Theorem statements to display their proofs.

Proof Structure

The Coq proof is split up into the following modules:

  • Definitions.v: The main inductive definitions and functions that are used in the proof. Defines the abstract syntax and type system.
  • Binding.v: Proves helper lemmas related to opening, closing, and local closure.
  • SubEnvironments.v: Defines and proves lemmas related to subenvironments.
  • Weakening.v: Proves the Weakening Lemma.
  • RecordAndInertTypes.v: Defines and proves lemmas related to record and inert types.
  • Narrowing.v: Proves the Narrowing Lemma.
  • OperationalSemantics.v: Defines normal forms and the operational semantics of DOT, as well as related helper lemmas.
  • PreciseTyping.v: Defines and proves lemmas related to precise typing. In particular, reasons about the possible precise types that a variable can have in an inert environment.
  • TightTyping.v: Defines tight typing and subtyping.
  • Substitution.v: Proves the Substitution Lemma.
  • InvertibleTyping.v: Defines invertible typing and proves that in an inert context, tight typing implies invertible typing (both for variables and values).
  • GeneralToTight.v: Proves that in an inert context, general typing implies tight typing.
  • CanonicalForms.v: Proves the Canonical Forms Lemmas for functions and objects.
  • Safety.v: Proves the Progress and Preservation Theorems.

The following figure shows a dependency graph between the Coq modules. Dependency graph

Evaluation Contexts vs. Runtime Environments

On paper, DOT's operational semantics is defined in terms of evaluation contexts. A type-soundness proof based on that semantics can be found in the proof-ec directory.

Evaluation contexts introduce complexity into the proof, which can be avoided by using an alternative semantics that is based on stacks.

A stack is a sequence of variable-to-value bindings, which serves as a runtime environment (in the literature, stacks are commonly referred to as stores). In the stack representation, the operational semantics is defined on pairs (s, t), where s is a stack and t is a term. For example, the term let x1 = v1 in let x1 = v2 in t is represented as ({(x1, v1), (x2, v2)}, t).

Compiling the Proof

To compile the proof, we require coq 8.6 and related tooling to be run in a unix-like environment. In particular, we require the following tools (all version 8.6) in the PATH enviroment variable:

  • coqc
  • coqtop
  • coqdep
  • coqdoc
  • coqmakefile

Other requirements are:

  • make

To compile the proof, run

git clone https://github.com/amaurremi/dot-calculus
cd dot-calculus/src/simple-proof
make

make will do the following:

  • compile the tlc library
  • compile the safety proof
  • generate documentation.