From: "Dan'l Miller" <optikos@verizon.net>
Subject: Re: Why not Coq2Ada program extraction?
Date: Sun, 6 May 2018 20:50:26 -0700 (PDT)
Date: 2018-05-06T20:50:26-07:00 [thread overview]
Message-ID: <5164e095-5d87-405d-93c9-9045dcc2fb01@googlegroups.com> (raw)
In-Reply-To: <87a7tc5gyh.fsf@nightsong.com>
On Sunday, May 6, 2018 at 9:37:27 PM UTC-5, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > As it turns out Coq isn't the only one to have made progress in
> > program-verification-based/proof-based
> > decompilation/reverse-engineering of machine code. Isabelle/HOL
>
> The concept of "extraction" doesn't make as much sense with Isabelle
> since it's not a programming language in the way Coq is.
But HOL4 and HOL-omega are. They are standard ML.
> You might like:
>
> http://concrete-semantics.org
Thank you. I have downloaded the free PDF of that book at:
http://concrete-semantics.org/concrete-semantics.pdf
next prev parent reply other threads:[~2018-05-07 3:50 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-05-01 3:38 Why not Coq2Ada program extraction? Dan'l Miller
2018-05-01 3:59 ` Paul Rubin
2018-05-01 6:59 ` Chris M Moore
2018-05-01 7:41 ` Paul Rubin
2018-05-01 11:44 ` Jere
2018-05-02 16:47 ` G.B.
2018-05-02 17:12 ` Paul Rubin
2018-05-01 8:21 ` Jeffrey R. Carter
2018-05-01 17:30 ` Dan'l Miller
2018-05-01 9:12 ` Paul Rubin
2018-05-07 2:30 ` Dan'l Miller
2018-05-07 2:37 ` Paul Rubin
2018-05-07 3:50 ` Dan'l Miller [this message]
2018-05-07 4:01 ` Dan'l Miller
2018-05-07 4:20 ` Paul Rubin
2018-05-07 16:33 ` Dan'l Miller
2018-05-07 13:27 ` Dan'l Miller
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox