Description
Name-binding & alpha-equivalence.
Description
Nominal-flavoured implementation of data in a context of local names, following the ideas in a new approach to abstract syntax with variable binding (see also author's pdfs). The recommended landing page is Language.Nominal, so please go there first. See also: a tutorial in Language.Nominal.Examples.Tutorial; a short development of untyped lambda-calculus in Language.Nominal.Examples.UntypedLambda; an example development of System F in Language.Nominal.Examples.SystemF; and an example development of an EUTxO-style blockchain in Language.Nominal.Examples.IdealisedEUTxO.