Titolo: 
A HOAS-based encoding of Typed Ambients in Coq

Autori: 
Marino Miculan and Ivan Scagnetto

We present a work in progress, extending [MS02], about a higher-order
encoding in the system Coq of the typed Ambient Calculus introduced in
[CGG00]. Since the latter is a nominal calculus, i.e., a formal system
based upon the notion of name, the Higher-Order Abstract Syntax
approach allows to formally represent it in an elegant and purified
way, delegating to the metalanguage the machinery of alpha-conversion,
capture avoiding substitution of names for names and schemata
instantiation.  In order to give a smooth formal representation of the
typing judgment, we first rephrased the original system in Natural
Deduction style in order to delegate to the Coq metalanguage the
tedious treatment of typing environments and the related machinery
(e.g. swapping of type declarations). An interesting outcome of this
approach is a substantial simplification in the proof of subject
reduction since the number of auxiliary lemmata is greatly reduced. In
particular, the whole development is built upon some rewriting results
stating the invariance of the typing judgment w.r.t. the replacement
of names with fresh ones having the same type. This is where the
Theory of Contexts [HMS01] plays a fundamental role allowing a smooth
treatment of those rewriting results.

[CGG00] Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon
        Types for the Ambient Calculus.
        To Appear in I&C special issue on TCS'2000.

[HMS01] Furio Honsell, Marino Miculan, Ivan Scagnetto
        An axiomatic approach to metareasoning on systems in 
        higher-order abstract syntax.
        In Proceedings of ICALP'01, Number 2076 in Lecture Notes in
        Computer Science, pages 963-978, 2001.

[MS02]  Marino Miculan and Ivan Scagnetto
        Ambient Calculus and its Logic in the Calculus of Inductive
        Constructions.
        In Proceedings of LFM 2002. ENTCS 70.2, Elsevier, 2002.