System FR

Description

This project aims to formalize in the Rocq Prover part of the Stainless project. It describes a call-by-value lambda-calculus and defines a rich type system (based on computations) that describes behaviors of lambda-calculus terms. Supported types include: System F polymorphism, recursive types, infinite intersections, refinement and dependent types, equality types.

Requirements

The proofs require Rocq and Rocq-Equations, which can be installed using opam:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam pin add -yn rocq-prover 9.0.0
opam install rocq-equations.1.3.1+9.0 -y

See “Installing the Rocq Prover and its packages” for more details.

Docker

Alternatively, you can also use the provided Dockerfile to build a Docker image with all dependencies installed:

docker build -t systemfr .
docker run -v "$(pwd)":/theories systemfr

Compiling the Proofs

After installing Rocq, you can compile the proofs using:

./configure
make -j8     # should take around 10 minutes

Overview of the proofs

All trees (for terms and for types) are defined in Trees.v. The operational semantics is given in SmallStep.v. The semantic definition of types is given in ReducibilityDefinition.v. We then prove soundness of inference rules for these types in the Erased*.v files (for erased terms) and in the Annotated*.v files (for annotated terms).

The file dependencies.pdf has an overview of the dependencies between all files.

Proofs for Scala Dependent Types project

We prove the following properties and the soundness of the typing rules. We rely on the following assumptions:

• The terms and types appearing in goals/context satisfy some well-formedness conditions
• The types are appearing in goals/context are non-empty
• Inferred types are always syntactically singletons
• During delta-beta reduction, the term being evaluated has type T_top (or equivalently, another arbitrary type)
• In untangle (Untangle.v), we know which terms have the Tau property, and we rely on the abstract model of update and tlookup specified using axioms in TauProperty.v

Properties

• widen gives a larger type widen_open_subtype in InferApp.v
• delta_beta_reduction gives observationally equivalent terms: delta_beta_obs_equiv in DeltaBetaReduction.v
• untangle returns an equivalent type untangle_open_equivalent_types in Untangle.v

Normalization Rules

• NBase: open_nbase1 and open_nbase2 in NormalizationBase.v
• NExists1: open_nexists_1 in NormalizationExists.v
• NExists2: open_nexists_2 in NormalizationExists.v
• NPi: open_npi in NormalizationPi.v
• NCons: open_ncons in NormalizationList.v
• NSing: open_nsing in NormalizationSing.v
• NMatch1: open_nmatch_1 in NormalizationMatch.v
• NMatch2: open_nmatch_2 in NormalizationMatch.v
• NMatch3: open_nmatch_3 in NormalizationMatch.v

Inference Rules

• TVar: open_tvar in InferMisc.v
• TAbs: open_tabs in InferMisc.v
• TApp: open_tapp in InferApp.v
• TLet open_tlet in InferApp.v
• TNil: open_tnil in ErasedList.v
• TCons: open_tcons in ErasedList.v
• TDots: open_append_key in TauProperty.v
• TFix: open_tfix in InferFix.v
• TMatch: open_tmatch in InferMatch.v
• TCheck: open_subtype_reducible in ReducibilitySubtype.v

Subtyping Rules

• SubTop: open_subtype in SubtypeMisc.v
• SubRefl: open_subrefl in SubtypeMisc.v
• SubSing: open_subsing in SubtypeMisc.v
• SubCons1: open_subcons1 in SubtypeList.v
• SubCons2: open_subcons2 in SubtypeList.v
• SubPi: open_subpi in SubtypePi.v
• SubExistsLeft: open_sub_exists_left in SubtypeExists
• SubExistsRight: open_sub_exists_right in SubtypeExists
• SubMatch: open_submatch in SubtypeMatch.v
• SubNorm: open_subnorm in SubtypeNorm.v