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 18:21:26 +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-f175.google.com
Ironport-phdr: 9a23:5mS0Wxy0FGg/V1zXCy+O+j09IxM/srCxBDY+r6Qd2+kWIJqq85mqBkHD//Il1AaPBtSEraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsLxUb05Vzav4qlyRBP0hyoMKjo1/WHLhsB1iq9QvRCvqAFlw4PMfY+bKvR+cKPec90US2VOUcReWDBODI6nc4sCDfAMMfpEo4TzpVYDqwa1Cwm2BOPozz9FnmH73akg1OQkDw7G2hAgEMoUvnTVsNX5LbkfUeSvw6nV0DrMcfdW0ir65YfUahAhoO2MUq50ccXL1EkgCh3KjlGLpIzqOjOazOUNs2yB4+V8UuKvjncqpgdsqTahwccsj5PGhoMTyl3c6Sp5wJw6Jce3SE5mf9GkCoFftzyHOIdsRcMiWW5otSAnwbMFoZ62ZDYGxIgjyhLFaPGKc5KE7g/9WOuSOzt0mXBodbKnixqv70StyffwW8263VpQrSdIk8PAum0M2hHV98OJUOFy/l271jaKzw3T6v9LIUQzlafDLp4u2L8wlp4KvUXNBC/6hFz6jKGLekgm+uWk8evnYrLhpp+TM497lBvyPbgpmsy6Geg4Mw4OUHaH+emkyrHv4Un0TK9Jg/A2iKXVrY7WKMcBqqKkAQJY0p4v6xOlADen1NQYk2MHLFVAeB+fk4fpI1DOIOzkAve7mVusjSpkyO7CPrD6DZXNK2LMkLblfbpn90Fczw8zwchF551IErEBPO7zWkjpudPECR85KhW4zPrjCNVgzYwTQnmPA6+cMKPKq1CE/OMvI++WZI8UojnxMfYl5+S9xUM+zFQaZOyi2YYdQHG+BPVvZUuDMlT2hdJUOmOLuwc4UNvSiUHHejpaenq/W+po7Sk6FImiBJrPS4SFj7mI3SP9FZpTMDMVQmuQGGvlIt3XE8wHbzifd5I5nw==

On 2017-07-17 18:04, Kevin Sullivan wrote:
> Pointers to any relevant work would be much appreciated,

You may be interested in http://www.chargueraud.org/softs/cfml/

[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