Module Kado

The kado library implements the syntax and semantics of cofibrations as described by ABCFHL.

Syntax

module Syntax : module type of Syntax

The abstract syntax of the restricted predicate logic of cofibrations.

module Builder : module type of Builder

Smart constructors.

Decision Procedures

module Theory : module type of Theory

The Theory module implements decision procedures for sequents relative to a theory over the interval, stated in the language of cofibrations.