Ott 0.10.15 (and previous versions) uses a fullyconcrete
representation for metavariables. It is up to the user to define
the appropriate fullyconcrete representation type for metavariables, e.g.:
metavar var,x ::= {{ coq nat }} {{ com term variable }}
metavar tvar,X ::= {{ coq nat }} {{ com type variable }}
Version 0.10.16 extends the Coq backend of Ott with experimental
support for a locallynameless representation (and cofinite quantification). The user can
now specify that a metavariable must be represented in
locallynameless style, e.g.:
metavar var,x ::= {{ reprlocallynameless }} {{ com term variable }}
As usual, metavariables can be bound in productions, using the
bindspec language, as in the lam production below:
grammar
term,t :: 'term_' ::= {{ com term }}
 x :: :: var {{ com variable }}
 \ x . t :: :: lam (+ bind x in t +) {{ com abstraction }}
 t1 t2 :: :: app {{ com application }}
 ( t ) :: S :: paren {{ coq [[t]] }}
 { t1 / x } t2 :: M :: tsub {{ coq (open_term_wrt_term[[x t2]] [[t1]]) }}
This definition gives rise to the datatype term below:
Inductive term : Set :=
 term_var_b : nat > term
 term_var_f : var > term
 term_lam : term > term
 term_app : term > term > term.
Remarks:
 Productions containing metavariables susceptible to be bound
(e.g., term_var) give rise to two distinct constructors,
one (term_var_b) for de Bruijn indices to be used when
the metavariable is bound, one (term_var_f) for "free"
variables. The type var, together with decidable
equality and several useful lemmas and functions, is defined in
the Metatheory library.
In the current implementation, metavariables susceptible to be
bound in a symbolic term (eg. the x in
the term_var production) must be the only element of the
production: in our experience, this did not turn out to be a
restriction, but please let us know if your language definition
requires more flexibility.
 Binder metavariables are erased from productions
(eg. term_lam), as in de Bruijn representation.
Ott automatically generates the appropriate open functions
and lc predicates to test if terms are locallyclosed.
The other support functions for substitutions and freevariables
(subst and fv) are generated once the user declares
the relevant substitutions and freevars sections.
Ott automatically compiles the symbolic terms that appear in rule
definitions into the appropriate terms in locallynameless style. For
instance, the typing rule for the simplytyped lambdacalculus:
E,x:S  t : T
 :: lambda
E  \x.t : S>T
is compiled into its locallynameless representation:
Inductive typing : env > term > type > Prop := (* defn typing
*)
 ...
 typing_lambda : forall (L:vars) (E:env) (t:term) (S T:type),
(forall x, x \notin L > typing (E & x ~ S) (open_term_wrt_term t (term_var_f x)) T) >
typing E (term_lam t) (type_arrow S T).
For that, Ott follows the algorithm below. For each rule,
 for each nonterminal that appears in the rule, compute the
maximal set of binders under which it appears: for example, in the
rule lambda above, the maximal set of binders for the
nonterminal t is the singleton x, and it is
empty for all the other nonterminals;
 for each pair nonterminal / maximal binder set collected in
phase 1., go over all the occurrences of the nonterminal in the
rule and open them with respect to all the variables in the
maximal binding set except those under which this particular
occurrence is bound. In the example, this amounts to opening the
occurrence of t in the premise with respect to the
metavariable x;
 quantify using cofinitequantification each metavariable that
has been used to open a nonterminal;
 add hypothesis about localclosure to guarantee the invariant
that if a derivation holds, then the toplevel terms involved are
locallyclosed.
In some cases the user may want a finer control on which nonterminals
are opened and with respect to which metavariables. Consider for
instance the CBV betareduction rule:
 :: ax_app
(\x.t1) v2 > {v2/x}t1
A naive application of the algorithm described above would open the
right hand side occurrence of t1 with respect to a
cofinitelyquantified x. Substitution should then be used to
replace the occurrences of x with v2, resulting in
the awkward term
reduce (term_app (term_lam t1) v2) (subst_term v2 x (open_term_wrt_term t1 (term_var_f x)))
Instead, an idiomatic translation of CBV betareduction rule would directly
rely on the open function to substitute v2 for the
bound occurrences of x in t1, as in:
reduce (term_app (term_lam t1) v2) (open_term_wrt_term t1 v2)
To let the user specify this translation behaviour, Ott 0.10.16 extends the syntax
of production homomorphisms. Consider:
term,t :: 'term_' ::= ...
 { t2 / x } t1 :: M :: tsub {{ coq (open_term_wrt_term [[x t1]] [[t2]]) }}
In the homomorphism the nonterminal t1 is referred to
with [[x t1]] instead of the usual [[t1]]: the
prefixed x specifies that occurrences of t1 should
not be opened with respect to the metavariable x. If this
homomorphism is specified, then the translation of the ax_app
rule is exactly idiomatic Coq shown above.
Current limitations: support for single binders only, no auxfn,
Coq only.
Disclaimer: to compile rule definitions, Ott applies blindly
the algorithm described above. Although in most of the cases, this
generates a correct and idiomatic representation of the language, some
language constructs might not be faithfully translated. Please, let us
know if you find one of these cases.
Some examples:
 STLC:
ott source,
pdf output,
coq output,
progress and preservation.

STLC, full reductions:
ott source,
pdf output,
coq output,
progress and preservation.

STLC + references:
ott source,
pdf output,
coq output.

STLC + tuples (dot forms):
ott source,
pdf output,
coq output.

Fsub:
ott source,
pdf output,
coq output.

Pitts and Stark's nucalculus, following Benton and Koutavas:
ott source,
pdf output,
coq output.
The generated Coq code requires the Metatheory library by Arthur Charguéraud.
The proof scripts are straightforward adaptations of
the analogous
scripts by Arthur Charguéraud. It would be easy to adapt
Charguéraud's proofs for Fsub and Benton and Kouvatas' proofs
for the nucalculus.
