coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Explicit substitutions

From: Flavio de Moura <flaviomoura AT unb.br>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]Explicit substitutions
Date: Tue, 14 Mar 2006 13:42:11 -0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

I am interested in explicit substitutions and, I am looking for some paper that explains how Coq deal with higher-order unification. Does it use explicit substitutions? If so, which calculus is implemented? Any paper (or comments) in this direction is very appreciated.

Best regards,

Flavio de Moura.

[Coq-Club]Explicit substitutions, Flavio de Moura