coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bas Spitters <b.a.w.spitters AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Functional programs in coq
- Date: Sat, 14 Apr 2018 16:32:56 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb0-f169.google.com
- Ironport-phdr: 9a23:5957HhQCuiehAdR2592zzGguENpsv+yvbD5Q0YIujvd0So/mwa6yYh2N2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRBDI2ybIUBEvQPMvpDoonhu1cDtweyCRWwCO7tzDJDm3/43bc90+QkCQzLwRYvH8kTu3rJtNX1NbsSUfyrw6nS1jXIcvRb1izn5IfSaBwgr+uAXaloccrQ1UkvCx3Kjk+LqYH+MDOV0/4Cs2mf7+Z6Se2vjGsnphh3rzOyyMksjYzJiZgUylDC7Sh5x5o6Kse9SE5/e9KkF4FQty6CO4RqQsMtWXtouCknyrIYo560ZjUKx4k9yx7YcfyHfJCE4h3iVOaNITd4mWlqdKijiBa19Eis0un8VtO10FpQoCpFiN/BvW0O2RzL8sWLVOdx80O71TuM1w3f8P9ILV06mKbBNpIsw7o9m5wOukrZBCD2gl/5jKqOe0Uk5Oeo7+Pnb63jppCGNo90jhjyM6Q1lcCjGOg4PBUCUmmf9Oim273j+kr5QLpOjvIoiKXWrJfaJcEDqq64BQ9azJoj5g6hAzu61NkUh3oKIVJfdB6ZkoTkNUvCLO35APq7m1islS1kx/HCPr3vGJXNKX3Dna/6crpn8UFQ0gQywcpE55JMC7EBPO7zVVHrtNzDFRI5PAm0zPzmCNV5zI8RRWWPAqqBPKPIrVCI/v4vI/WLZIINpDn9LOEl6+fygn89hF8SZrKk3YAXaXC9BvRpOV+VYXvqgtcbEGcFpBAyTOLwiA7KbTkGTHGrF4k4+ztzXImhFMLIQp2nqL2HxiayWJNMMDNoEFeJRF3hbM2/Q/YQdC+IOYc1mHoNE6fnUJcgyQ2jrhTSxL9uL+6S8Sod48GwnONp7vHewElhvQd/CN6QhiTUFzktzzE4AgQu1aU6mnRTj1KK0Kx2mftdTIUB6PZAUwN8PpnZnbUjV4LCHznZd9LMc26IB828CGhoHN00yt4KJU16Hof6102R72+RG7YQ0oezKtk0/6bbhSajIs98zzPX3vFkgQB4E41AMmqpgqM5/A/WVdbE
What is currently the best way of importing pure/total functional
programs into Coq?
I know I can write them in Coq directly, but I would like to interact
with other programs too.
For ocaml, I am aware of:
https://vocal.lri.fr/ (The library does not seem to be available)
https://ocaml.org/meetings/ocaml/2014/ocaml2014_15.pdf
CFML (coq 8.5)
http://www.chargueraud.org/softs/cfml/
However, these seem to focus on non-functional parts too.
For haskell there is:
https://github.com/antalsz/hs-to-coq
Are there better options?
Thanks,
Bas
- [Coq-Club] Functional programs in coq, Bas Spitters, 04/14/2018
Archive powered by MHonArc 2.6.18.