coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Second order logic library?

From: Anders Lundstedt <anders AT anderslundstedt.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Second order logic library?
Date: Fri, 24 Mar 2017 13:59:47 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=anders AT anderslundstedt.se; spf=Pass smtp.mailfrom=anders AT anderslundstedt.se; spf=None smtp.helo=postmaster AT mail-lf0-f46.google.com
Ironport-phdr: 9a23:03MRRBOJW7j8HW985O4l6mtUPXoX/o7sNwtQ0KIMzox0LfTzrarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAB/z5LObY2JKPZyYqHQcNUHTmRBRMZRUClBD5ugYosJEuUOI/xYr5LgrFUIsBu+AxSjBPjzyjBWm3D2wbAx3uM7HgHAwQMvAcgOsG/PodrvMqcdTP66zLPTzTXHcvNW3yry6JPUch8/vP6MQah8cdHPxkQ2EQ7Ok1ueqYvgPzyP1+QNtXCW7+VhVeKzi24nthp+riKzyccrj4nEgJ8exFPc9Shh3oo5Odm1RFR4bNOkCpdcqTyWOotsTs4tQmxlvjsxxKcctp6hZicKzYwqxx7BZPyDdIiF+hfjW/yQITd8nX5lfLy/iwqr/UiuxeDxV9O40FlNripCndnMsm4C2wbP5ciAT/tx5kah2TCR2ADP8uxIP1w4mK7BJ5MiwrM8jIQfvVnDEyPsl0j7jbeadkA+9eip7+TnbK/mppiZN4JskA7+NLkhldKlAeQjKQUBRW6b9vmi27355k35RKhKjvsrnanCrJDVO9kUprKjDw9OzIkv8wy/ACu+0NQEgXkHK0pIdw6Aj4jwIl3BPPT4DeqkjFm3izdqx/XGPqX7DZnXL3jDlq3hfbdn5EJGxgoz14MX25UBQLoGObf4XlL7nN3eFB4wdQKuia6zA9Jkk4gaRGinA6mDMaqUv0Xetcw1JOzZTYkZtSzmY9w44fL1kXI1hRdJdK+l0IEMQHm+Evl8OEGEZ3b3ntoNDSERs1xtH6TRlFSeXGsLND6JVKUm62RjBQ==

I needed a deep embedding of first-order arithmetic some time ago. In
the end I wrote my own. See in particular the file
"heytingarithmetic.v" at

https://github.com/anderslundstedt/pca-realizability

I tailored the embedding quite heavily to my own needs, but perhaps
the definitions can be adapted for a more general setting.

[Coq-Club] Second order logic library?, Caitlin McGregor, 03/23/2017
- Re: [Coq-Club] Second order logic library?, Adam Chlipala, 03/23/2017
  - Re: [Coq-Club] Second order logic library?, Caitlin McGregor, 03/23/2017
    - Re: [Coq-Club] Second order logic library?, Pierre Courtieu, 03/23/2017
      - Re: [Coq-Club] Second order logic library?, Caitlin McGregor, 03/23/2017
        
        Re: [Coq-Club] Second order logic library?, Asya Bergal, 03/23/2017
        
        Re: [Coq-Club] Second order logic library?, Asya Bergal, 03/23/2017
        
        Re: [Coq-Club] Second order logic library?, Anders Lundstedt, 03/24/2017
        Re: [Coq-Club] Second order logic library?, Caitlin McGregor, 03/27/2017