coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Beta Ziliani <beta AT mpi-sws.org>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] PLT Redex -> Coq
- Date: Mon, 9 May 2016 15:48:34 -0300
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
- Ironport-phdr: 9a23:K15IZR/M6pcBwv9uRHKM819IXTAuvvDOBiVQ1KB91e0cTK2v8tzYMVDF4r011RmSDdSdsqgP0rCP+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U1p78jrrrs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOf7Ubl8azWm7q5tSVe8giobPhY86GCSkdNryqVBr0Ty9FRE34fIbdTNZ7JFdaTHcIZfHDIZUw==
Hi list,
A colleague of mine used PLT Redex to define a language and its semantics, but now he wants to prove some properties of X in Coq. He's wondering if there is a tool to translate PLT Redex definitions into Coq ones, or if he should write all of them from scartch.
A colleague of mine used PLT Redex to define a language and its semantics, but now he wants to prove some properties of X in Coq. He's wondering if there is a tool to translate PLT Redex definitions into Coq ones, or if he should write all of them from scartch.
Thanks!
Beta
- [Coq-Club] PLT Redex -> Coq, Beta Ziliani, 05/09/2016
- Re: [Coq-Club] PLT Redex -> Coq, William J. Bowman, 05/09/2016
Archive powered by MHonArc 2.6.18.