coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Second order logic library?
Date: Wed, 22 Mar 2017 20:06:44 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:q/sm9hc8gPEc7r1FcAYASLsUlGMj4u6mDksu8pMizoh2WeGdxcu4bR7h7PlgxGXEQZ/co6odzbGH7+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5br5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37X/ZisJwgqxYrhyuqRNwzIzIb4yOLvVyYrnQcMkGSWdPXstcUTFKDIOmb4sICuoMJfpVoJTnqFsLsBCzGwmsBOfuyj9QnHD22bc12PkmHA7cwQMvBdcOv2jPodrpL6cdS+G1zK3SwTXGbvNWxS3x55bVfRA8uPyBW697f8nJyUQ3Cg/JkFadpZbrMj+JzOgBrXKX4/R9We6zk2IqqRx9riKxysoihITFnJ8Zx1DG+Clj3oo5ONO1RUhmatC+CpRQrTuVN45uT8MiXW5ovCE6x6UBuZ6mYCgKx5Mnxx/Za/yIaoSI+Q7jW/yNIThinn5qZKm/iAyz8Uik0OH8U8i00EpQoiVbj9bMq2gB1x3V6seZVvtw5lqt1SiM2gzJ5OxIPVo4mbTBJ5I/37I8ioIfsUHZES/3nEX2grWWdkIh+uWw8evof6/pppqAOIJvlg7+Kb4hms27AegiNwgOXnSb9f6i27L+4E31WK9KgeEukqnFrJDaItwWqbK+Aw9My4os9xK/Dyq939kDhnkGLFdFeAqdgITzOlHOJur4DfaljFi2njdr3aOOArq0CZLUa3PHjb3JfLBn6kcaxhBg48pY4sd9BrgEaNnzXk7pvdjRRkswPwWxyM7sE9x80sUbWH7JD6OEZvCB+WSU7/4idrHfLLQevyzwfqAo

What exactly would be in such a library, considering that, in a reasonable sense, second-order logic is a subset of Coq's full logic?

On 03/22/2017 08:03 PM, Caitlin McGregor wrote:

Hi all,

I am looking for a second order logic library in Coq, or even a first order library. Does anyone know if these are available?

Thanks in advance,

Caitlin

[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