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