Titolo:
A type sound formalization of imp-$\varsigma$ in Coq

Autori:
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan

We encode the Abadi-Cardelli's imp-$\varsigma$ calculus
in Coq using an higher-order approach. We formalize
the syntax, the first-order static semantics and the
big-step dynamic semantics. The ultimate goal is to
obtain a Type Soundness result in Coq.