Stream: Coq users

Topic: Coq and semantics


view this post on Zulip MMY MMY (Aug 27 2022 at 11:39):

Hello,
I am very new to Coq.
As part of a project, I need to create denotational semantics and test it with Coq.
I'm trying to transform a piece of code into Coq but I don't know how!

Below is the part of the sematics and my test in Coq:

image.png

Definition assignment (var:Exp)( e:Exp) (rhoF :Envf )(rho:Env )(s:State)(Ks :Cs): mSStm :=
let (K0e : Ce) := (v0 , s0) => Ks((rho var) -> v0)
in let (v1,s1) := mExp e rhoF rho s K0e
in s1 .

view this post on Zulip Paolo Giarrusso (Aug 27 2022 at 13:25):

For prospective answerers — see cross-post in https://coq.discourse.group/t/coq-and-denotational-semantics/1771.
(Cross-posting like this isn't encouraged, FWIW).

view this post on Zulip Paolo Giarrusso (Aug 27 2022 at 13:47):

I'm sorry I can't help myself, but I'm not sure what else you've written, how much you know etc. Googling for "denotational semantics in Coq" found https://jhc.sjtu.edu.cn/public/courses/CS263/ which has some notes on a simple denotational semantics.

view this post on Zulip Alexander Gryzlov (Aug 27 2022 at 13:55):

@Jonathan Sterling has the https://github.com/jonsterling/coq-domains library which might help in formalizing denotational stuff (DCPOs etc).

view this post on Zulip Alexander Gryzlov (Aug 27 2022 at 14:02):

Also, there's a short module on den. sem. in this course: https://github.com/xavierleroy/cdf-mech-sem

view this post on Zulip Karl Palmskog (Aug 27 2022 at 16:05):

There might be code on denotational semantics here: https://github.com/coq-community/semantics

view this post on Zulip MMY MMY (Aug 27 2022 at 17:35):

Thanks a lot for your answers.

view this post on Zulip MMY MMY (Aug 27 2022 at 18:22):

I have seen the majority of the references.
I think that's far from what I'm doing.

How can I translate:

K0e of type Ce equal to the torque (v0 , s0).

view this post on Zulip Paolo Giarrusso (Aug 27 2022 at 19:29):

There does not seem to be enough context to answer the question well.


Last updated: Jan 31 2023 at 14:03 UTC