coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] PLT Redex -> Coq

From: "William J. Bowman" <wjb AT williamjbowman.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] PLT Redex -> Coq
Date: Mon, 9 May 2016 15:13:34 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=wjb AT williamjbowman.com; spf=Pass smtp.mailfrom=wjb AT williamjbowman.com; spf=None smtp.helo=postmaster AT mail.williamjbowman.com
Ironport-phdr: 9a23:vI/n7Ree98SZb14V0tJcCuVrlGMj4u6mDksu8pMizoh2WeGdxc6+Yx7h7PlgxGXEQZ/co6odzbGG4ua5AydZu8/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuKOU4R3mP1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBD2CVJBwzE5RSyfNG5mCzls+N7kmHOIs/8Za81XTCj5qJpQhj3jS4BcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==

You may want to CC
racket-users AT googlegroups.com;
Redex experts there may also know.

--
William J. Bowman

On Mon, May 09, 2016 at 03:48:34PM -0300, Beta Ziliani wrote:
> 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.
>
> Thanks!
> Beta

Attachment: signature.asc
Description: PGP signature

[Coq-Club] PLT Redex -> Coq, Beta Ziliani, 05/09/2016
- Re: [Coq-Club] PLT Redex -> Coq, William J. Bowman, 05/09/2016