Skip to content

A Coq module for working with linear typing contexts.

Notifications You must be signed in to change notification settings

inQWIRE/LinearTypingContexts

Repository files navigation

This repository contains a framework for reasoning about linear typing contexts in Coq.

The file Monoid.v describes the algebraic structure of partial commutative monoids, which are characterized by the following parts:

  • A base type "A"
  • A unit element "⊤ : A"
  • An undefined element "⊥ : A"
  • A merge operation, written "a ∙ b"

Partial commutative monoids satisfy the following laws:

  • (A,⊤,∙) forms a commutative monoid
  • a ∙ ⊥ = ⊥

The tactic monoid solves goals of the form a = b, where a and b are made up of PCM constructors and at most one EVar.

The file TypingContext.v describes additional structure on top of PCM's. A typing context "Ctx" with domain "X" and image "A" satisfies:

  • Ctx is a partial commutative monoid
  • for x:X and a:A, a singleton context singleton x a : Ctx
  • for any context Γ:Ctx, a predicate is_valid Γ that checks if Γ is the undefined element ⊥.

The tactic validate solves goals of the form is_valid Γ. It is based on the following principles:

  • (Γ₁ ∙ Γ₂ ∙ Γ₃) is valid if and only if all of (Γ₁ ∙ Γ₂), (Γ₁ ∙ Γ₃), and (Γ₂ ∙ Γ₃) are valid.
  • ⊤ is valid
  • the singleton context (x,a) is valid
  • for two singletons (x,a) and (y,b), the context singleton x a ∙ singleton y b is valid if and only if x <> y.

We give the following instantiation of the TypingContext type class:

  • IndexContext.v: Contexts are list (option T) where variables are natural numbers that index into a list

About

A Coq module for working with linear typing contexts.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published