coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Caitlin McGregor <caitlin.mcgregor AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Second order logic library?
Date: Mon, 27 Mar 2017 02:58:05 +0000
Accept-language: en-AU, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caitlin.mcgregor AT anu.edu.au; spf=Pass smtp.mailfrom=caitlin.mcgregor AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:Tb0mRBZwbD1tkEnh/XFUAmL/LSx+4OfEezUN459isYplN5qZr8S4bnLW6fgltlLVR4KTs6sC0LuK9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhKvpRN/wpLbb46OOfVkYq/RYckXSXZdUspPUSFKH4Oyb5EID+oEJetVsZPyp1oSrRu6BAmsAv7kxDhUiXH3x601zeshEQbc3Ac9GN8BrG7brNTpNKcWUOC1yrPEzTDfYPNZwzfy9ofIchc7ofyXR71wd9fRxVMxGAzYk1Wcs5bqPy6M2+kLrmOV4e1gVee1hG4mrQF8ujevxsYwionJm4Ia0UrI+jl+wIYwI9CzVU11Yca8HZdNqy2XOJF6T8wgTm1ypSo217wLtYSmcCQXy5kr3wPTZvKbf4SS4h/uVfydLSlliH9qYr6zmhS//Emmx+bhTMe7ykxKoTBAktTUtnACyRjT6s+fR/Zh8EivxCqD2x3K5u9DLk44iLPXK5k6zbEujJYTtlnDHjPtl0Xxka+WcFgr9vKw6+T9ZbXmuoGTOJNoigH/NaQunNazAeMlMggSW2ib/uO81L758ULlR7VKi+U6kqjfsJ/EOcQWvrO1DxNa34o55BuyDS2q3MkFkXQGNl5JZQ+LgovxN1HLOv/4DPO/g1q2kDdswvDLJqHuDY/MLnjflLfhfLB951RZyAUvwtBf/YxbCr4GIPLpQUL+rtrYDgIjPwOq3unnFc9x2ZkDWW6XGK+WLLvSsUOU5uIoO+SDeIgVuC/kJ/c54/7ukGQ2lEQGfaip2JsXcGq3Eu5nI0Wfe3rsg80OHX0EvgokH6TWjwjIWjlKIn22QqgU5zchCYvgA52JDtSmh6XE1yOmFLVXYHpHAxaCCyG7WZ+DXqInYSOOJs5n2hkPeqKsRIg7nUWlvQ7mz7thaO/f9TcVupX5/NFz+qvemQx0/CEiXJfV6H2EU2whxjBAfDQxxq0q+UE=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi,

Thanks for your responses, and apologies for the delay in mine.

Indeed, a deep embedding is what I'm after - thank you for providing the phrase to express what I was after. And thank you both for attaching excerpts of your code. It's a little surprising to me that there isn't a standard or general library available, as opposed to individual's tailored formulation.

Anyway! Thanks again for your help.

All the best,
Caitlin

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Anders Lundstedt <anders AT anderslundstedt.se>
Sent: Friday, 24 March 2017 11:59:47 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Second order logic library?

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