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:

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 .

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).

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.

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

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

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

Thanks a lot for your answers.

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).

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

Last updated: Jan 31 2023 at 14:03 UTC