coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lifting programs into Coq

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lifting programs into Coq
Date: Mon, 17 Jul 2017 23:33:44 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f170.google.com
Ironport-phdr: 9a23:gyLRrBP47bkmM5s2Mwwl6mtUPXoX/o7sNwtQ0KIMzox0Lfn8rarrMEGX3/hxlliBBdydsKMbzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkaKTA5/mHZhM9+gq1Vrx2upQBwzYHPbYGJNvdzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cMI+JYqJP4p1QQqxu+GRGjCvnuyj9Un3P7w6k63P48EQ7bwgMgG88FvXPIo9XtNacSTfy6zK3SwjXecvxZxzP95ZPHchAku/6MXLZwfdDNxkkoEgPIl1OdopHmMTONzukBrXSX4u56We+si2MrsRx9riasy8s2l4XEhJ4ZxkjZ+SllxIs5P8O0RUFhbdK6DpddtzuWOoR4T84kXmpmojw1yqcctp6+ZCUKyIooxxrYa/GfdoiH+BPjVOKILTZ2nnJpZKuzhxiv/UWi1uHwTMa00FFNripKltnDqGoB2ADU6siCUvd9/0Gh1iiT1w3L9O1IPUQ5mbDYJpMh2LI8i4QfvEfZEiPrmkj6kLeadkA+9eip7+TnbK/mppiZN4Jslg7+KqUumtCjDuQ8KAcOQnWU9vq41LD48k35Ra9FjvwykqXDrJ/aIsEbqrajAwBJyoYj9wq/DzC+3dsEmnkHNUtJdw6Dj4j0IF7DO+v4DPe6g1S0ijhn3fHGPrv7ApXMNHfPirnhfawuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsGAg1xuvhFOJF159bcmaGH6OUNOuGukeJ+ukrKvSAaYs9tzP0Kvxj7Pnr2yxq0WQBdLWkiMNEIEuzGe5rdh2U

On 2017-07-17 21:58, Kevin Sullivan wrote:
> You've solved a harder problem! We're happy to have this pointer.

Well, Arthur did; I wasn't involved in this work.

[Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
- Re: [Coq-Club] Lifting programs into Coq, Adam Chlipala, 07/17/2017
  - Re: [Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
- Re: [Coq-Club] Lifting programs into Coq, Clément Pit-Claudel, 07/17/2017
  - Re: [Coq-Club] Lifting programs into Coq, Tej Chajed, 07/17/2017
    - Re: [Coq-Club] Lifting programs into Coq, Pierre Courtieu, 07/17/2017
      - Re: [Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
  - Re: [Coq-Club] Lifting programs into Coq, Kevin Sullivan, 07/17/2017
    - Re: [Coq-Club] Lifting programs into Coq, Clément Pit-Claudel, 07/17/2017