coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Formalization of the syntax of first-order logic: binders

From: Alan Schmitt <alan.schmitt AT polytechnique.org>
To: Jason Hu <fdhzs2010 AT hotmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Formalization of the syntax of first-order logic: binders
Date: Tue, 12 Oct 2021 09:04:54 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=Pass smtp.pra=alan.schmitt AT polytechnique.org; spf=Pass smtp.mailfrom=SRS0=AOsY=PA=polytechnique.org=alan.schmitt AT bounces.m4x.org; spf=Pass smtp.helo=postmaster AT mx1.polytechnique.org
Ironport-hdrordr: A9a23:uIkxL6i05WnZquWBeuqBD1LT9nBQXv8ji2hC6mlwRA09TyX4rayTdZsguiMc5Ax+ZJhCo7290cu7MBDhHPdOiOF7V4tKNzOHhILHFuBfBMfZsljdMhy73eoY8adkbqRkTPz5ClV+gcuS2njdL/8QhPKCtJ2yjeDF1nF3UEVWa6Vt9RpwDh/zKDwQeOEXbaBJdqah2g==
Ironport-phdr: A9a23:6s8elB9ZMc8dKP9uWQS7ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZAqOvL4w0xfgZsby07p8ke3YsqTtCyQrwK2qlzQ8SqFKTAIPks4MngYtU4avAEz/K+P2PWRhRJwRHFBq8GumPkdLBc3we0PdomGo7T4VBx7zKRd5Kv76F4LMk8i7zeS/94DcbwhIhje2fK9/IgixoQjNrMcdnJFsKrw2yhvHo3tIf/pZyGZ1Ll+NnBjy+9m98od7/ytfp/wu+chAUb7nf6sjVrxXEC4mM2Eu68L1sxTIUBaC6WEdUmUSlRpIHhTF4RTnVZr/rif2quxw0zScMMbrT747RC6i4r9rRhH2lSkINTA5/m/UhMN/kK1Wux2hqwBlzoPOfI2ZKOZyc6XAdt0aX2pBWcNRWjRdD4O4dYQPCfcKM/tEoIn9olsOrAe+BRWxD+7o0DBIgmX53asg3+Q6DQ7G3AkgH9MSsHTIt9j1LKASUeS1zanU0zrMc/NW2TH86IjRbxAuv+uAXbVqccre0EQiER7OgVqMp4L/JTyVyvgNvHaB7+pmTe+hhG4ppQ5yrzWyyMkhiZfFi5wJx1zZ6Cl0zog4KcC2RkN/btOqHodcuSGeOoZyTM0vQ2Jltig+x7AFtpC2YicHxZI6zBDRbPyHdpKH4hPlVOuJIDd4gmhleLOliBqo/0ig0OvxXdS33lZStidJj8fAu3QX2xDO9sSKReFx80m91TqV2Q3e5flILV06mKbGMZIt3L49m5UJvUjeAiP6glj6ga2Kekgi5+Om8f7oYq/8qZ+ZL4J0ih/xMqApmsGnBOQ5PRUCU3KD+eS70L3i/VH5T6tWgf02lKnZsYnaJdkFqaKjBA9VyIkj5w6+DzegztsYgWEKIE9bdB+DlYTlJk3CLf/iAfqxn1igijlmyv/eMr3kGJrNL3zDkLn7fbZ67k5R0Bc9w8xC6Z5IErwMPOv9WlTzu9HAFBE0LxS5w/7gCNV51oIeRXyADbOZMKPUsF+I//8vLPeWaI8Sojb9JOAo6OTqjXAjn18RZ7Kp0ocXaHC9H/RmP1mZbGH3jdcGDGcKuBYxQ/LxiFGYVD5eaHmzU7g75jEhB4KqFZ3DSZy1gLydwCe7GYVbaXxBClCVCHvna4GEW+oXZy+JOc9gkjkEVaC7RIM71BGushX6y7t9IebO9C0Yr8Gr6N8gxeTIkhd61SE8W8qR03OWFTktxksIQCMz1aF750d6zwHHmeJzhOUdHthO7dtIVB07PNjS1aYyX9v1Q0fKesqDYFegWNSvRz8rGIEf2dgLNm95EtPqtRvD2iu2H/dBnriCAtov+aLZ3mTtD956z2fa2aIhiVg/X8YJMnep0P0svzPPDpLExh3K352hcr4RiXalHIirx22TukpVS0h1DbWDWmoQNBK+RTXR41ObCaepDaU7PwBBz8+bN6YMbcfm3wwurBLLINPacn68kGe2BA+Vy/WLdoW4Ig0g

On 2021-10-12 02:13, Jason Hu <fdhzs2010 AT hotmail.com> writes:

> I would like to add that IMO, de Bruijn indices reflect the paper
> proof the most faithfully, among the three methods mentioned here and
> probably others.

We compared several methods (locally nameless, nominal, weak HOAS, and
full de Bruijn) in a completely different setting (a process calculus
with two kinds of binders and scope extrusion), and we found the most
concise method was de Bruijn, although they each have some advantages
and drawbacks. The work is available at
https://hal.inria.fr/hal-02536463v2/file/jar.pdf

Best,

Alan

Attachment: signature.asc
Description: PGP signature

[Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/11/2021
- Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Wilayat Khan, 10/11/2021
  - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Pierre Courtieu, 10/11/2021
    - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Carlos Olarte, 10/11/2021
      - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/12/2021
        
        RE: [Coq-Club] Formalization of the syntax of first-order logic: binders, Jason Hu, 10/12/2021
        
        RE: [Coq-Club] Formalization of the syntax of first-order logic: binders, Alan Schmitt, 10/12/2021
        
        Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Dominik Kirst, 10/12/2021
        Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/14/2021