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: Dominik Kirst <dominik.kirst AT cs.uni-saarland.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Formalization of the syntax of first-order logic: binders
Date: Tue, 12 Oct 2021 17:38:59 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dominik.kirst AT cs.uni-saarland.de; spf=Pass smtp.mailfrom=dominik.kirst AT cs.uni-saarland.de; spf=None smtp.helo=postmaster AT theia.rz.uni-saarland.de
Ironport-hdrordr: A9a23:MYqUZ69zMxbIo/3YGf1uk+DJI+orL9Y04lQ7vn2ZOiYlF/Bw9vre/sjzuiWUtN98Yh0dcLO7Scq9qBHnm6KdiLN5VdyftW/d0ldAR7sM0WKN+VDd8mHFltJg6Q==
Ironport-phdr: A9a23:vAdVXhAjQy1JvAF6UotmUyQUJ0QY04WdBeb1wqQuh78GSKm/5ZOqZBWZua81yg6QFtiEo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6u95HJZwhEmTWxbLNwIR6rsQjfq84ajJd4JK0s0BXJuHxIe+pXxWNsO12emgv369mz8pB+7Sleouot+MFcX6r0eaQ4VqFYAy89M28p/s3rtALMQhWJ63ABT2gZiBtIAwzC7BHnQpf8tzbxu+Rh1CWGO8D9ULY5Uimg4ah2Uh/lkCcJOCI2/2/KhMJwgrxVrxCiqRJ42IPbep2ZNP9kc6PdYd8XR2xMVdtRWSxbBYO8apMCAeQGPeZdron9oVoOrRijDgepBePv0CRIhmPr1qA9zushFgTG3A0mH9IPs3TYttb1NKYIUeCu0KnF1inMb+hM1Tfg7ojIcwktoeqWUr1qa8rRzVMgFwXYgVmKtIPqISqY2+IQuGeU8+RuT/igi3I7qw5vuDivwN8hh4nIi48R1FzJ9yp3zYU7KNO4VUJ2f9CqHZtMuyyVKYd4TMMvTn1otSs117ELp4C2cSwWxJkpxxDSaf6KfoeG7x/lSe2fLzB4hHd/d7K+gRa/6VOgyuzzVsms1FZFtCxFnsPLtnAX2Bzf8smHSv1n/kegwzmDzQ7T6vtCLEsplqTbM4YszqM+m5ccq0jOGi77lF/0gaOMeEgo5/Ck5uf5brn8uJOQK415hhvgPqkgmMGzG/k0PwsTU2Wd5O+yyaXj8lf8QLtJlv07irTVvZ7VKMgBoqO0AhVZ34Q55xuxEjur1skTk2MdI1JfYh2HipDkO1HQL/D8Cveym0iskDd1yPDHJLLtGI/NL3nZnLf8e7Z96ldQyBEpwt9F/ZJUDqsOIPTuVUPrqdPXEAc1Mw2yw+n5FNVwzp4SVGyAD6ODNK7fsEWE6+A1L+SCeYMZoDP9JOIk5/7qg385g1gdfayx0JQKb3C4G/VmI0OYYXrvmNsBEmYKvhAlTOz2k1CNTSVTa2yvX6I65zE3EZmmAp3ZSYC3hLyOxiG7EYBMam9bFF+ACW3oeJmcW/cQdCKSJddsnSADVbi4UoMuyRWutBLhxLd8NerV+igYtYr529Rv5u3Tkwsy9T1uAMiH3WGNVTI8omRdTDgvmat7vEZVy1GZ0KE+jeYLO8ZU4qZlVQI7M5/fh897EcvuElbNedKITlelBNanGyotZtkqhcIIYgNmEty4ihnF02ymDulGxPSwGJUo//eEjDDKLMFnxiOevEHAp0UmT8pGc3e0wLN59k3IDofTl0yfm+CmePZEtMYo3GyYi3eIvQRDWQdqVazDUTYTaxmOxTwWzkjZCaKoCPE8OwJbzceEJu1GZ4+w5Wg=

Just to add one more option: there is also Olivier Laurent’s anti-locally-nameless approach.

https://popl21.sigplan.org/details/CPP-2021/17/An-Anti-Locally-Nameless-Approach-to-Formalizing-Quantifiers

Best,

Dominik

On 12. Oct 2021, at 09:04, Alan Schmitt <alan.schmitt AT polytechnique.org> wrote:

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

[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