This repository contains various versions of the semantics of the untyped lambda calculus plus extensions for the verse programming language.

verse syntax (well-scoped de Bruijn representation, generated by autosubst)

verse/syntax.v

verse equational theory (based on ICFP reduction rules)

verse/icfp.v

step based denotational semantics

stepverse/densem.v -- just sets values, no order stepverse/densemLabeledResult.v -- sets of labeled results

graph-model denotational semantics

graphverse/definitions.v graphverse/congruence_theory.v graphverse/valid_theory.v graphverse/denot.v
graphverse/consistency.v graphverse/continuity.v graphverse/subst.v graphverse/theory.v

untyped lambda calculus syntax (locally-nameless representation)

syntax

lc/lc_inf.v lc/lc_ott.v lc/tactics.v lc/scoped.v

denotational semantics

simple/model.v

library for defining semantic operations

structures/Comp.v structures/Env.v structures/List.v structures/Sets.v structures/Monad.v structures/Option.v structures/FSet.v structures/NFSet.v structures/Structures.v structures/consistency.v verse/axioms.v -- from autosubst verse/fintype.v -- from autosubst, with extensions

denot/properties.v denot/list_properties.v denot/nelist_properties.v