Blist 
List operations.

Hashset 
This module implements imperative sets as hash tables.

Lru 
Implementation of an LRU cache for memoising functions.

Sigs 
Core module signatures used in Cyclist.

Soundcheck 
Provides an abstract view of a proof as a graph and allows checking its
soundness.

Proofnode 
A node in a cyclic proof.

Proofrule 
A proofrule used by a cyclic prover.

Proof 
A cyclic proof object.

Prover 
A cyclic prover object.

Seqtactics 
Tactics for combining sequentlevel rules.

Abdrule 
An abduction rule used in an abductive cyclic prover.

Abducer 
A cyclic abducer (cf.

Ord_constraints 
A structure representing a set of constraints on ordinalvalued variables.

Utilsigs 
Signatures for containers and essential types.

Flist 
A functorised list.

Multiset 
A multiset container.

Listset 
A listbased set container.

Treemap 
An ordered map using the standard
Map module.

Pair 
Operations on pairs.

Treeset 
An ordered container based on the standard
Set module.

Containers 
Given a
BasicType build a module with several containers for it.

Strng 
String
BasicType with assorted containers.

Int 
Int
BasicType with assorted containers.

Fun 
Combinators for manipulating functions.

Option 
Functions for manipulating optional values.

Tags 
A set of tags.

Tagpairs 
A set of tag pairs with a few convenience functions.

Unification 
A library of types and combinators supporting
continuationpassingstyle unifiers

VarManager 
An abstract datatype for managing variables.

Sl_abduce 
This module contains functions to answer various abduction questions for
use in program verification.

Sl_term 
Module defining SL terms, which consist of variables (free
or existentially quantified), or the constant
nil .

Sl_subst 
Module providing SL term substitutionrelated functionality.

Sl_unify 
This module specialises the generic Unification module to the SL
instantiation of cyclist and provides extra functionality to support the
unification of its various elements

Sl_tpair 
An ordered pair of SL terms.

Sl_uf 
A unionfind structure for SL terms.

Sl_rho 
A stack structure for prophecy variables.

Sl_deqs 
Sets of disequalities over terms.

Sl_pto 
Pointsto atom, consisting of a pair of a term and a list of terms.

Sl_ptos 
Multiset of pointstos.

Sl_pred 
Predicate occurrences consisting of a predicate identifier and a list of
terms as parameters.

Sl_tpred 
Tagged predicate, as a pair of an integer and a predicate.

Sl_tpreds 
Multiset of tagged predicates.

Sl_heap 
Symbolic heaps.

Sl_heap_rho 
Symbolic heaps.

Sl_form 
SL formula, basically a list of symbolic heaps, denoting their disjunction,
along with a set of contraints on predicate ordinal labels (tags).

Sl_form_rho 
SL formula, basically a list of symbolic heaps, denoting their disjunction.

Sl_seq 
SL sequent, as a pair of SL formulas.

Sl_indrule 
Inductive rule type consisting of a symbolic heap and a predicate head.

Tl_form 
A CTL temporal logic formula

Tl_form_ltl 
An LTL temporal logic formula
